0 JBC
↳1 JBCToGraph (⇒, 710 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
↳5 JBCTerminationSCC
↳6 SCCToIDPv1Proof (⇒, 1720 ms)
↳7 IDP
↳8 IDPNonInfProof (⇒, 750 ms)
↳9 AND
↳10 IDP
↳11 IDependencyGraphProof (⇔, 0 ms)
↳12 IDP
↳13 UsableRulesProof (⇔, 0 ms)
↳14 IDP
↳15 IDPNonInfProof (⇒, 2290 ms)
↳16 IDP
↳17 IDependencyGraphProof (⇔, 0 ms)
↳18 TRUE
↳19 IDP
↳20 IDependencyGraphProof (⇔, 0 ms)
↳21 IDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 IDP
↳24 IDPNonInfProof (⇒, 2480 ms)
↳25 IDP
↳26 IDependencyGraphProof (⇔, 0 ms)
↳27 TRUE
↳28 JBCTerminationSCC
↳29 SCCToIDPv1Proof (⇒, 150 ms)
↳30 IDP
↳31 IDPNonInfProof (⇒, 130 ms)
↳32 AND
↳33 IDP
↳34 IDependencyGraphProof (⇔, 0 ms)
↳35 TRUE
↳36 IDP
↳37 IDependencyGraphProof (⇔, 0 ms)
↳38 TRUE
package BinarySearch;
public class BinarySearch {
public static void main(String[] argv) {
Random.args = argv;
int[] data = createArray();
binarySearch(data, Random.random());
}
public static boolean binarySearch(int[] data, int val) {
return binarySearch(data, val, 0, data.length);
}
private static boolean binarySearch(int[] data, int val, int l, int u) {
if (l > u) {
return false;
}
int mid = l + (u - l)/2;
if (data[mid] == val) {
return true;
} else {
if (binarySearch(data, val, l, mid - 1)) {
return true;
}
return binarySearch(data, val, mid + 1, u);
}
}
public static int[] createArray() {
int[] data = new int[Random.random()];
for (int i = 0; i < data.length; i++) {
data[i] = Random.random();
}
return data;
}
}
package BinarySearch;
public class Random {
static String[] args;
static int index = 0;
public static int random() {
final String string = args[index];
index++;
return string.length();
}
}
Generated 58 rules for P and 105 rules for R.
P rules:
1869_0_binarySearch_Load(EOS(STATIC_1869), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542) → 1871_0_binarySearch_LE(EOS(STATIC_1871), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543)
1871_0_binarySearch_LE(EOS(STATIC_1871), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543) → 1872_0_binarySearch_LE(EOS(STATIC_1872), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543)
1872_0_binarySearch_LE(EOS(STATIC_1872), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543) → 1875_0_binarySearch_Load(EOS(STATIC_1875), java.lang.Object(ARRAY(i540)), i541, i542, i543) | <=(i542, i543)
1875_0_binarySearch_Load(EOS(STATIC_1875), java.lang.Object(ARRAY(i540)), i541, i542, i543) → 1878_0_binarySearch_Load(EOS(STATIC_1878), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542)
1878_0_binarySearch_Load(EOS(STATIC_1878), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542) → 1882_0_binarySearch_Load(EOS(STATIC_1882), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543)
1882_0_binarySearch_Load(EOS(STATIC_1882), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543) → 1885_0_binarySearch_IntArithmetic(EOS(STATIC_1885), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543, i542)
1885_0_binarySearch_IntArithmetic(EOS(STATIC_1885), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543, i542) → 1891_0_binarySearch_ConstantStackPush(EOS(STATIC_1891), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, -(i543, i542))
1891_0_binarySearch_ConstantStackPush(EOS(STATIC_1891), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i555) → 1894_0_binarySearch_IntArithmetic(EOS(STATIC_1894), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i555, 2)
1894_0_binarySearch_IntArithmetic(EOS(STATIC_1894), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i555, matching1) → 1899_0_binarySearch_IntArithmetic(EOS(STATIC_1899), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, /(i555, 2)) | =(matching1, 2)
1899_0_binarySearch_IntArithmetic(EOS(STATIC_1899), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i558) → 1902_0_binarySearch_Store(EOS(STATIC_1902), java.lang.Object(ARRAY(i540)), i541, i542, i543, +(i542, i558))
1902_0_binarySearch_Store(EOS(STATIC_1902), java.lang.Object(ARRAY(i540)), i541, i542, i543, i561) → 1907_0_binarySearch_Load(EOS(STATIC_1907), java.lang.Object(ARRAY(i540)), i541, i542, i543, i561)
1907_0_binarySearch_Load(EOS(STATIC_1907), java.lang.Object(ARRAY(i540)), i541, i542, i543, i561) → 1910_0_binarySearch_Load(EOS(STATIC_1910), java.lang.Object(ARRAY(i540)), i541, i542, i543, i561, java.lang.Object(ARRAY(i540)))
1910_0_binarySearch_Load(EOS(STATIC_1910), java.lang.Object(ARRAY(i540)), i541, i542, i543, i561, java.lang.Object(ARRAY(i540))) → 1912_0_binarySearch_ArrayAccess(EOS(STATIC_1912), java.lang.Object(ARRAY(i540)), i541, i542, i543, i561, java.lang.Object(ARRAY(i540)), i561)
1912_0_binarySearch_ArrayAccess(EOS(STATIC_1912), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1915_0_binarySearch_ArrayAccess(EOS(STATIC_1915), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1915_0_binarySearch_ArrayAccess(EOS(STATIC_1915), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1919_0_binarySearch_ArrayAccess(EOS(STATIC_1919), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1919_0_binarySearch_ArrayAccess(EOS(STATIC_1919), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1921_0_binarySearch_Load(EOS(STATIC_1921), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, i568) | <(i567, i540)
1921_0_binarySearch_Load(EOS(STATIC_1921), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, i568) → 1925_0_binarySearch_NE(EOS(STATIC_1925), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, i568, i541)
1925_0_binarySearch_NE(EOS(STATIC_1925), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, i568, i541) → 1927_0_binarySearch_NE(EOS(STATIC_1927), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, i568, i541)
1927_0_binarySearch_NE(EOS(STATIC_1927), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, i568, i541) → 1934_0_binarySearch_Load(EOS(STATIC_1934), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567) | !(=(i568, i541))
1934_0_binarySearch_Load(EOS(STATIC_1934), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567) → 1940_0_binarySearch_Load(EOS(STATIC_1940), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)))
1940_0_binarySearch_Load(EOS(STATIC_1940), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540))) → 1945_0_binarySearch_Load(EOS(STATIC_1945), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i541)
1945_0_binarySearch_Load(EOS(STATIC_1945), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i541) → 1951_0_binarySearch_Load(EOS(STATIC_1951), java.lang.Object(ARRAY(i540)), i541, i543, i567, java.lang.Object(ARRAY(i540)), i541, i542)
1951_0_binarySearch_Load(EOS(STATIC_1951), java.lang.Object(ARRAY(i540)), i541, i543, i567, java.lang.Object(ARRAY(i540)), i541, i542) → 1959_0_binarySearch_ConstantStackPush(EOS(STATIC_1959), java.lang.Object(ARRAY(i540)), i541, i543, i567, java.lang.Object(ARRAY(i540)), i541, i542, i567)
1959_0_binarySearch_ConstantStackPush(EOS(STATIC_1959), java.lang.Object(ARRAY(i540)), i541, i543, i567, java.lang.Object(ARRAY(i540)), i541, i542, i567) → 1965_0_binarySearch_IntArithmetic(EOS(STATIC_1965), java.lang.Object(ARRAY(i540)), i541, i543, i567, java.lang.Object(ARRAY(i540)), i541, i542, i567, 1)
1965_0_binarySearch_IntArithmetic(EOS(STATIC_1965), java.lang.Object(ARRAY(i540)), i541, i543, i567, java.lang.Object(ARRAY(i540)), i541, i542, i567, matching1) → 1970_0_binarySearch_InvokeMethod(EOS(STATIC_1970), java.lang.Object(ARRAY(i540)), i541, i543, i567, java.lang.Object(ARRAY(i540)), i541, i542, -(i567, 1)) | &&(>=(i567, 0), =(matching1, 1))
1970_0_binarySearch_InvokeMethod(EOS(STATIC_1970), java.lang.Object(ARRAY(i540)), i541, i543, i567, java.lang.Object(ARRAY(i540)), i541, i542, i579) → 1975_1_binarySearch_InvokeMethod(1975_0_binarySearch_Load(EOS(STATIC_1975), java.lang.Object(ARRAY(i540)), i541, i542, i579), java.lang.Object(ARRAY(i540)), i541, i543, i567, java.lang.Object(ARRAY(i540)), i541, i542, i579)
1975_0_binarySearch_Load(EOS(STATIC_1975), java.lang.Object(ARRAY(i540)), i541, i542, i579) → 1980_0_binarySearch_Load(EOS(STATIC_1980), java.lang.Object(ARRAY(i540)), i541, i542, i579)
1975_1_binarySearch_InvokeMethod(1880_0_binarySearch_Return(EOS(STATIC_1880), java.lang.Object(ARRAY(i588)), i589, i590, i591, matching1), java.lang.Object(ARRAY(i588)), i589, i543, i567, java.lang.Object(ARRAY(i588)), i589, i590, i591) → 1997_0_binarySearch_Return(EOS(STATIC_1997), java.lang.Object(ARRAY(i588)), i589, i543, i567, java.lang.Object(ARRAY(i588)), i589, i590, i591, java.lang.Object(ARRAY(i588)), i589, i590, i591, 0) | =(matching1, 0)
1975_1_binarySearch_InvokeMethod(1942_0_binarySearch_Return(EOS(STATIC_1942), java.lang.Object(ARRAY(i601)), i602, i603, i604, i597, matching1), java.lang.Object(ARRAY(i601)), i602, i543, i567, java.lang.Object(ARRAY(i601)), i602, i603, i604) → 1998_0_binarySearch_Return(EOS(STATIC_1998), java.lang.Object(ARRAY(i601)), i602, i543, i567, java.lang.Object(ARRAY(i601)), i602, i603, i604, java.lang.Object(ARRAY(i601)), i602, i603, i604, i597, 1) | =(matching1, 1)
1975_1_binarySearch_InvokeMethod(2294_0_binarySearch_Return(EOS(STATIC_2294), java.lang.Object(ARRAY(i1099)), i1100, i1102, i1098, matching1), java.lang.Object(ARRAY(i1099)), i1100, i543, i567, java.lang.Object(ARRAY(i1099)), i1100, i1101, i1102) → 2332_0_binarySearch_Return(EOS(STATIC_2332), java.lang.Object(ARRAY(i1099)), i1100, i543, i567, java.lang.Object(ARRAY(i1099)), i1100, i1101, i1102, java.lang.Object(ARRAY(i1099)), i1100, i1102, i1098, 1) | =(matching1, 1)
1975_1_binarySearch_InvokeMethod(2385_0_binarySearch_Return(EOS(STATIC_2385), matching1), java.lang.Object(ARRAY(i1294)), i1295, i543, i567, java.lang.Object(ARRAY(i1294)), i1295, i1296, i1297) → 2440_0_binarySearch_Return(EOS(STATIC_2440), java.lang.Object(ARRAY(i1294)), i1295, i543, i567, java.lang.Object(ARRAY(i1294)), i1295, i1296, i1297, 0) | =(matching1, 0)
1975_1_binarySearch_InvokeMethod(2397_0_binarySearch_Return(EOS(STATIC_2397), matching1), java.lang.Object(ARRAY(i1330)), i1331, i543, i567, java.lang.Object(ARRAY(i1330)), i1331, i1332, i1333) → 2448_0_binarySearch_Return(EOS(STATIC_2448), java.lang.Object(ARRAY(i1330)), i1331, i543, i567, java.lang.Object(ARRAY(i1330)), i1331, i1332, i1333, 1) | =(matching1, 1)
1975_1_binarySearch_InvokeMethod(2473_0_binarySearch_Return(EOS(STATIC_2473), i1372), java.lang.Object(ARRAY(i1522)), i1523, i543, i567, java.lang.Object(ARRAY(i1522)), i1523, i1524, i1525) → 2543_0_binarySearch_Return(EOS(STATIC_2543), java.lang.Object(ARRAY(i1522)), i1523, i543, i567, java.lang.Object(ARRAY(i1522)), i1523, i1524, i1525, i1372)
1980_0_binarySearch_Load(EOS(STATIC_1980), java.lang.Object(ARRAY(i540)), i541, i542, i579) → 1865_0_binarySearch_Load(EOS(STATIC_1865), java.lang.Object(ARRAY(i540)), i541, i542, i579)
1865_0_binarySearch_Load(EOS(STATIC_1865), java.lang.Object(ARRAY(i540)), i541, i542, i543) → 1869_0_binarySearch_Load(EOS(STATIC_1869), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542)
1997_0_binarySearch_Return(EOS(STATIC_1997), java.lang.Object(ARRAY(i588)), i589, i543, i567, java.lang.Object(ARRAY(i588)), i589, i590, i591, java.lang.Object(ARRAY(i588)), i589, i590, i591, matching1) → 2004_0_binarySearch_EQ(EOS(STATIC_2004), java.lang.Object(ARRAY(i588)), i589, i543, i567, 0) | =(matching1, 0)
2004_0_binarySearch_EQ(EOS(STATIC_2004), java.lang.Object(ARRAY(i588)), i589, i543, i567, matching1) → 2261_0_binarySearch_EQ(EOS(STATIC_2261), java.lang.Object(ARRAY(i588)), i589, i543, i567, 0) | =(matching1, 0)
2261_0_binarySearch_EQ(EOS(STATIC_2261), java.lang.Object(ARRAY(i1013)), i1014, i543, i567, matching1) → 2277_0_binarySearch_EQ(EOS(STATIC_2277), java.lang.Object(ARRAY(i1013)), i1014, i543, i567, 0) | =(matching1, 0)
2277_0_binarySearch_EQ(EOS(STATIC_2277), java.lang.Object(ARRAY(i1013)), i1014, i543, i567, matching1) → 2283_0_binarySearch_Load(EOS(STATIC_2283), java.lang.Object(ARRAY(i1013)), i1014, i543, i567) | =(matching1, 0)
2283_0_binarySearch_Load(EOS(STATIC_2283), java.lang.Object(ARRAY(i1013)), i1014, i543, i567) → 2296_0_binarySearch_Load(EOS(STATIC_2296), i1014, i543, i567, java.lang.Object(ARRAY(i1013)))
2296_0_binarySearch_Load(EOS(STATIC_2296), i1014, i543, i567, java.lang.Object(ARRAY(i1013))) → 2301_0_binarySearch_Load(EOS(STATIC_2301), i543, i567, java.lang.Object(ARRAY(i1013)), i1014)
2301_0_binarySearch_Load(EOS(STATIC_2301), i543, i567, java.lang.Object(ARRAY(i1013)), i1014) → 2319_0_binarySearch_ConstantStackPush(EOS(STATIC_2319), i543, java.lang.Object(ARRAY(i1013)), i1014, i567)
2319_0_binarySearch_ConstantStackPush(EOS(STATIC_2319), i543, java.lang.Object(ARRAY(i1013)), i1014, i567) → 2333_0_binarySearch_IntArithmetic(EOS(STATIC_2333), i543, java.lang.Object(ARRAY(i1013)), i1014, i567, 1)
2333_0_binarySearch_IntArithmetic(EOS(STATIC_2333), i543, java.lang.Object(ARRAY(i1013)), i1014, i567, matching1) → 2334_0_binarySearch_Load(EOS(STATIC_2334), i543, java.lang.Object(ARRAY(i1013)), i1014, +(i567, 1)) | &&(>=(i567, 0), =(matching1, 1))
2334_0_binarySearch_Load(EOS(STATIC_2334), i543, java.lang.Object(ARRAY(i1013)), i1014, i1130) → 2336_0_binarySearch_InvokeMethod(EOS(STATIC_2336), java.lang.Object(ARRAY(i1013)), i1014, i1130, i543)
2336_0_binarySearch_InvokeMethod(EOS(STATIC_2336), java.lang.Object(ARRAY(i1013)), i1014, i1130, i543) → 2337_1_binarySearch_InvokeMethod(2337_0_binarySearch_Load(EOS(STATIC_2337), java.lang.Object(ARRAY(i1013)), i1014, i1130, i543), java.lang.Object(ARRAY(i1013)), i1014, i1130, i543)
2337_0_binarySearch_Load(EOS(STATIC_2337), java.lang.Object(ARRAY(i1013)), i1014, i1130, i543) → 2339_0_binarySearch_Load(EOS(STATIC_2339), java.lang.Object(ARRAY(i1013)), i1014, i1130, i543)
2339_0_binarySearch_Load(EOS(STATIC_2339), java.lang.Object(ARRAY(i1013)), i1014, i1130, i543) → 1865_0_binarySearch_Load(EOS(STATIC_1865), java.lang.Object(ARRAY(i1013)), i1014, i1130, i543)
1998_0_binarySearch_Return(EOS(STATIC_1998), java.lang.Object(ARRAY(i601)), i602, i543, i567, java.lang.Object(ARRAY(i601)), i602, i603, i604, java.lang.Object(ARRAY(i601)), i602, i603, i604, i597, matching1) → 2006_0_binarySearch_EQ(EOS(STATIC_2006), java.lang.Object(ARRAY(i601)), i602, i543, i567, 1) | =(matching1, 1)
2006_0_binarySearch_EQ(EOS(STATIC_2006), java.lang.Object(ARRAY(i601)), i602, i543, i567, matching1) → 2059_0_binarySearch_EQ(EOS(STATIC_2059), java.lang.Object(ARRAY(i601)), i602, i543, i567, 1) | =(matching1, 1)
2059_0_binarySearch_EQ(EOS(STATIC_2059), java.lang.Object(ARRAY(i619)), i620, i543, i567, matching1) → 2261_0_binarySearch_EQ(EOS(STATIC_2261), java.lang.Object(ARRAY(i619)), i620, i543, i567, 1) | =(matching1, 1)
2332_0_binarySearch_Return(EOS(STATIC_2332), java.lang.Object(ARRAY(i1099)), i1100, i543, i567, java.lang.Object(ARRAY(i1099)), i1100, i1101, i1102, java.lang.Object(ARRAY(i1099)), i1100, i1102, i1098, matching1) → 2050_0_binarySearch_Return(EOS(STATIC_2050), java.lang.Object(ARRAY(i1099)), i1100, i543, i567, java.lang.Object(ARRAY(i1099)), i1100, i1101, i1102, java.lang.Object(ARRAY(i1099)), i1100, i1102, i1098, 1) | =(matching1, 1)
2050_0_binarySearch_Return(EOS(STATIC_2050), java.lang.Object(ARRAY(i619)), i620, i543, i567, java.lang.Object(ARRAY(i619)), i620, i621, i622, java.lang.Object(ARRAY(i619)), i620, i622, i618, matching1) → 2059_0_binarySearch_EQ(EOS(STATIC_2059), java.lang.Object(ARRAY(i619)), i620, i543, i567, 1) | =(matching1, 1)
2440_0_binarySearch_Return(EOS(STATIC_2440), java.lang.Object(ARRAY(i1294)), i1295, i543, i567, java.lang.Object(ARRAY(i1294)), i1295, i1296, i1297, matching1) → 2232_0_binarySearch_Return(EOS(STATIC_2232), java.lang.Object(ARRAY(i1294)), i1295, i543, i567, java.lang.Object(ARRAY(i1294)), i1295, i1296, i1297, 0) | =(matching1, 0)
2232_0_binarySearch_Return(EOS(STATIC_2232), java.lang.Object(ARRAY(i901)), i902, i543, i567, java.lang.Object(ARRAY(i901)), i902, i903, i907, i906) → 2260_0_binarySearch_EQ(EOS(STATIC_2260), java.lang.Object(ARRAY(i901)), i902, i543, i567, i906)
2260_0_binarySearch_EQ(EOS(STATIC_2260), java.lang.Object(ARRAY(i901)), i902, i543, i567, i906) → 2261_0_binarySearch_EQ(EOS(STATIC_2261), java.lang.Object(ARRAY(i901)), i902, i543, i567, i906)
2448_0_binarySearch_Return(EOS(STATIC_2448), java.lang.Object(ARRAY(i1330)), i1331, i543, i567, java.lang.Object(ARRAY(i1330)), i1331, i1332, i1333, matching1) → 2232_0_binarySearch_Return(EOS(STATIC_2232), java.lang.Object(ARRAY(i1330)), i1331, i543, i567, java.lang.Object(ARRAY(i1330)), i1331, i1332, i1333, 1) | =(matching1, 1)
2543_0_binarySearch_Return(EOS(STATIC_2543), java.lang.Object(ARRAY(i1522)), i1523, i543, i567, java.lang.Object(ARRAY(i1522)), i1523, i1524, i1525, i1372) → 2232_0_binarySearch_Return(EOS(STATIC_2232), java.lang.Object(ARRAY(i1522)), i1523, i543, i567, java.lang.Object(ARRAY(i1522)), i1523, i1524, i1525, i1372)
R rules:
1871_0_binarySearch_LE(EOS(STATIC_1871), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543) → 1874_0_binarySearch_LE(EOS(STATIC_1874), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543)
1874_0_binarySearch_LE(EOS(STATIC_1874), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543) → 1877_0_binarySearch_ConstantStackPush(EOS(STATIC_1877), java.lang.Object(ARRAY(i540)), i541, i542, i543) | >(i542, i543)
1877_0_binarySearch_ConstantStackPush(EOS(STATIC_1877), java.lang.Object(ARRAY(i540)), i541, i542, i543) → 1880_0_binarySearch_Return(EOS(STATIC_1880), java.lang.Object(ARRAY(i540)), i541, i542, i543, 0)
1912_0_binarySearch_ArrayAccess(EOS(STATIC_1912), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 1914_0_binarySearch_ArrayAccess(EOS(STATIC_1914), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
1914_0_binarySearch_ArrayAccess(EOS(STATIC_1914), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 1917_0_<init>_Load(EOS(STATIC_1917), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) | <=(i566, -1)
1915_0_binarySearch_ArrayAccess(EOS(STATIC_1915), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1920_0_binarySearch_ArrayAccess(EOS(STATIC_1920), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1917_0_<init>_Load(EOS(STATIC_1917), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 1924_0_<init>_InvokeMethod(EOS(STATIC_1924), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
1920_0_binarySearch_ArrayAccess(EOS(STATIC_1920), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1923_0_<init>_Load(EOS(STATIC_1923), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) | >=(i567, i540)
1923_0_<init>_Load(EOS(STATIC_1923), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1932_0_<init>_InvokeMethod(EOS(STATIC_1932), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1924_0_<init>_InvokeMethod(EOS(STATIC_1924), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 1926_0_<init>_Load(EOS(STATIC_1926), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
1925_0_binarySearch_NE(EOS(STATIC_1925), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, i541, i541) → 1928_0_binarySearch_NE(EOS(STATIC_1928), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, i541, i541)
1926_0_<init>_Load(EOS(STATIC_1926), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 1939_0_<init>_InvokeMethod(EOS(STATIC_1939), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
1928_0_binarySearch_NE(EOS(STATIC_1928), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, i541, i541) → 1935_0_binarySearch_ConstantStackPush(EOS(STATIC_1935), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567)
1932_0_<init>_InvokeMethod(EOS(STATIC_1932), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1937_0_<init>_Load(EOS(STATIC_1937), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1935_0_binarySearch_ConstantStackPush(EOS(STATIC_1935), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567) → 1942_0_binarySearch_Return(EOS(STATIC_1942), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, 1)
1937_0_<init>_Load(EOS(STATIC_1937), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1950_0_<init>_InvokeMethod(EOS(STATIC_1950), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1939_0_<init>_InvokeMethod(EOS(STATIC_1939), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 1944_0_<init>_Load(EOS(STATIC_1944), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
1944_0_<init>_Load(EOS(STATIC_1944), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 1957_0_<init>_InvokeMethod(EOS(STATIC_1957), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
1950_0_<init>_InvokeMethod(EOS(STATIC_1950), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1955_0_<init>_Load(EOS(STATIC_1955), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1955_0_<init>_Load(EOS(STATIC_1955), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1968_0_<init>_InvokeMethod(EOS(STATIC_1968), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1957_0_<init>_InvokeMethod(EOS(STATIC_1957), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 1964_0_<init>_Load(EOS(STATIC_1964), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
1964_0_<init>_Load(EOS(STATIC_1964), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 1974_0_<init>_InvokeMethod(EOS(STATIC_1974), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
1968_0_<init>_InvokeMethod(EOS(STATIC_1968), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1972_0_<init>_Load(EOS(STATIC_1972), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1972_0_<init>_Load(EOS(STATIC_1972), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1982_0_<init>_InvokeMethod(EOS(STATIC_1982), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1974_0_<init>_InvokeMethod(EOS(STATIC_1974), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 1977_0_<init>_Load(EOS(STATIC_1977), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
1975_1_binarySearch_InvokeMethod(2084_0_binarySearch_ArrayAccess(EOS(STATIC_2084), java.lang.Object(ARRAY(i712)), i713, i714, i715, i566, java.lang.Object(ARRAY(i712)), i566), java.lang.Object(ARRAY(i712)), i713, i543, i567, java.lang.Object(ARRAY(i712)), i713, i714, i715) → 2135_0_binarySearch_ArrayAccess(EOS(STATIC_2135), java.lang.Object(ARRAY(i712)), i713, i543, i567, java.lang.Object(ARRAY(i712)), i713, i714, i715, java.lang.Object(ARRAY(i712)), i713, i714, i715, i566, java.lang.Object(ARRAY(i712)), i566)
1975_1_binarySearch_InvokeMethod(2118_0_binarySearch_ArrayAccess(EOS(STATIC_2118), java.lang.Object(ARRAY(i751)), i752, i753, i754, i747, java.lang.Object(ARRAY(i751)), i747), java.lang.Object(ARRAY(i751)), i752, i543, i567, java.lang.Object(ARRAY(i751)), i752, i753, i754) → 2179_0_binarySearch_ArrayAccess(EOS(STATIC_2179), java.lang.Object(ARRAY(i751)), i752, i543, i567, java.lang.Object(ARRAY(i751)), i752, i753, i754, java.lang.Object(ARRAY(i751)), i752, i753, i754, i747, java.lang.Object(ARRAY(i751)), i747)
1975_1_binarySearch_InvokeMethod(2216_0_binarySearch_InvokeMethod(EOS(STATIC_2216), java.lang.Object(ARRAY(i1049)), i1050, i1052, i1048, java.lang.Object(ARRAY(i1049)), i1050, i1051, i785), java.lang.Object(ARRAY(i1049)), i1050, i543, i567, java.lang.Object(ARRAY(i1049)), i1050, i1051, i1052) → 2279_0_binarySearch_InvokeMethod(EOS(STATIC_2279), java.lang.Object(ARRAY(i1049)), i1050, i543, i567, java.lang.Object(ARRAY(i1049)), i1050, i1051, i1052, java.lang.Object(ARRAY(i1049)), i1050, i1052, i1048, java.lang.Object(ARRAY(i1049)), i1050, i1051, i785)
1975_1_binarySearch_InvokeMethod(2291_0_binarySearch_InvokeMethod(EOS(STATIC_2291), java.lang.Object(ARRAY(i1086)), i1087, i1089, i1085, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1052), java.lang.Object(ARRAY(i1086)), i1087, i543, i567, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1089) → 2327_0_binarySearch_InvokeMethod(EOS(STATIC_2327), java.lang.Object(ARRAY(i1086)), i1087, i543, i567, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1089, java.lang.Object(ARRAY(i1086)), i1087, i1089, i1085, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1052)
1975_1_binarySearch_InvokeMethod(2394_0_binarySearch_InvokeMethod(EOS(STATIC_2394), java.lang.Object(ARRAY(i1312)), i1313, i1168, i1315), java.lang.Object(ARRAY(i1312)), i1313, i543, i567, java.lang.Object(ARRAY(i1312)), i1313, i1314, i1315) → 2443_0_binarySearch_InvokeMethod(EOS(STATIC_2443), java.lang.Object(ARRAY(i1312)), i1313, i543, i567, java.lang.Object(ARRAY(i1312)), i1313, i1314, i1315, java.lang.Object(ARRAY(i1312)), i1313, i1168, i1315)
1975_1_binarySearch_InvokeMethod(2465_0_binarySearch_InvokeMethod(EOS(STATIC_2465), java.lang.Object(ARRAY(i1485)), i1486, i1488, i1484, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1315), java.lang.Object(ARRAY(i1485)), i1486, i543, i567, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1488) → 2525_0_binarySearch_InvokeMethod(EOS(STATIC_2525), java.lang.Object(ARRAY(i1485)), i1486, i543, i567, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1488, java.lang.Object(ARRAY(i1485)), i1486, i1488, i1484, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1315)
1975_1_binarySearch_InvokeMethod(2469_0_binarySearch_InvokeMethod(EOS(STATIC_2469), java.lang.Object(ARRAY(i1503)), i1504, i1321, i1506), java.lang.Object(ARRAY(i1503)), i1504, i543, i567, java.lang.Object(ARRAY(i1503)), i1504, i1505, i1506) → 2535_0_binarySearch_InvokeMethod(EOS(STATIC_2535), java.lang.Object(ARRAY(i1503)), i1504, i543, i567, java.lang.Object(ARRAY(i1503)), i1504, i1505, i1506, java.lang.Object(ARRAY(i1503)), i1504, i1321, i1506)
1977_0_<init>_Load(EOS(STATIC_1977), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 1986_0_<init>_InvokeMethod(EOS(STATIC_1986), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
1982_0_<init>_InvokeMethod(EOS(STATIC_1982), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1984_0_<init>_Load(EOS(STATIC_1984), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1984_0_<init>_Load(EOS(STATIC_1984), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2001_0_<init>_InvokeMethod(EOS(STATIC_2001), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1986_0_<init>_InvokeMethod(EOS(STATIC_1986), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 1996_0_<init>_Load(EOS(STATIC_1996), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
1996_0_<init>_Load(EOS(STATIC_1996), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 2003_0_<init>_Load(EOS(STATIC_2003), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
2001_0_<init>_InvokeMethod(EOS(STATIC_2001), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2009_0_<init>_Load(EOS(STATIC_2009), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2003_0_<init>_Load(EOS(STATIC_2003), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 2010_0_<init>_FieldAccess(EOS(STATIC_2010), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
2009_0_<init>_Load(EOS(STATIC_2009), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2016_0_<init>_Load(EOS(STATIC_2016), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2010_0_<init>_FieldAccess(EOS(STATIC_2010), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 2019_0_<init>_Load(EOS(STATIC_2019), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
2016_0_<init>_Load(EOS(STATIC_2016), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2023_0_<init>_FieldAccess(EOS(STATIC_2023), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2019_0_<init>_Load(EOS(STATIC_2019), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 2025_0_<init>_InvokeMethod(EOS(STATIC_2025), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
2023_0_<init>_FieldAccess(EOS(STATIC_2023), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2032_0_<init>_Load(EOS(STATIC_2032), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2025_0_<init>_InvokeMethod(EOS(STATIC_2025), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 2034_0_<init>_StackPop(EOS(STATIC_2034), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
2032_0_<init>_Load(EOS(STATIC_2032), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2043_0_<init>_InvokeMethod(EOS(STATIC_2043), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2034_0_<init>_StackPop(EOS(STATIC_2034), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 2045_0_<init>_Return(EOS(STATIC_2045), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
2043_0_<init>_InvokeMethod(EOS(STATIC_2043), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2052_0_<init>_StackPop(EOS(STATIC_2052), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2045_0_<init>_Return(EOS(STATIC_2045), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 2054_0_<init>_Return(EOS(STATIC_2054), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
2052_0_<init>_StackPop(EOS(STATIC_2052), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2061_0_<init>_Return(EOS(STATIC_2061), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2054_0_<init>_Return(EOS(STATIC_2054), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 2063_0_<init>_Return(EOS(STATIC_2063), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
2061_0_<init>_Return(EOS(STATIC_2061), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2068_0_<init>_Return(EOS(STATIC_2068), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2063_0_<init>_Return(EOS(STATIC_2063), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 2070_0_<init>_Return(EOS(STATIC_2070), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
2068_0_<init>_Return(EOS(STATIC_2068), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2075_0_<init>_Return(EOS(STATIC_2075), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2070_0_<init>_Return(EOS(STATIC_2070), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 2077_0_<init>_Return(EOS(STATIC_2077), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
2075_0_<init>_Return(EOS(STATIC_2075), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2082_0_<init>_Return(EOS(STATIC_2082), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2077_0_<init>_Return(EOS(STATIC_2077), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566) → 2084_0_binarySearch_ArrayAccess(EOS(STATIC_2084), java.lang.Object(ARRAY(i540)), i541, i542, i543, i566, java.lang.Object(ARRAY(i540)), i566)
2082_0_<init>_Return(EOS(STATIC_2082), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2092_0_<init>_Return(EOS(STATIC_2092), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2092_0_<init>_Return(EOS(STATIC_2092), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2118_0_binarySearch_ArrayAccess(EOS(STATIC_2118), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2135_0_binarySearch_ArrayAccess(EOS(STATIC_2135), java.lang.Object(ARRAY(i712)), i713, i543, i567, java.lang.Object(ARRAY(i712)), i713, i714, i715, java.lang.Object(ARRAY(i712)), i713, i714, i715, i566, java.lang.Object(ARRAY(i712)), i566) → 2180_0_binarySearch_ArrayAccess(EOS(STATIC_2180), java.lang.Object(ARRAY(i712)), i713, i543, i567, java.lang.Object(ARRAY(i712)), i713, i714, i715, java.lang.Object(ARRAY(i712)), i713, i714, i715, i566, java.lang.Object(ARRAY(i712)), i566)
2179_0_binarySearch_ArrayAccess(EOS(STATIC_2179), java.lang.Object(ARRAY(i751)), i752, i543, i567, java.lang.Object(ARRAY(i751)), i752, i753, i754, java.lang.Object(ARRAY(i751)), i752, i753, i754, i747, java.lang.Object(ARRAY(i751)), i747) → 2180_0_binarySearch_ArrayAccess(EOS(STATIC_2180), java.lang.Object(ARRAY(i751)), i752, i543, i567, java.lang.Object(ARRAY(i751)), i752, i753, i754, java.lang.Object(ARRAY(i751)), i752, i753, i754, i747, java.lang.Object(ARRAY(i751)), i747)
2180_0_binarySearch_ArrayAccess(EOS(STATIC_2180), java.lang.Object(ARRAY(i780)), i781, i543, i567, java.lang.Object(ARRAY(i780)), i781, i782, i785, java.lang.Object(ARRAY(i780)), i781, i782, i785, i786, java.lang.Object(ARRAY(i780)), i786) → 2216_0_binarySearch_InvokeMethod(EOS(STATIC_2216), java.lang.Object(ARRAY(i780)), i781, i543, i567, java.lang.Object(ARRAY(i780)), i781, i782, i785)
2216_0_binarySearch_InvokeMethod(EOS(STATIC_2216), java.lang.Object(ARRAY(i780)), i781, i543, i567, java.lang.Object(ARRAY(i780)), i781, i782, i785) → 2291_0_binarySearch_InvokeMethod(EOS(STATIC_2291), java.lang.Object(ARRAY(i780)), i781, i543, i567, java.lang.Object(ARRAY(i780)), i781, i782, i785)
2261_0_binarySearch_EQ(EOS(STATIC_2261), java.lang.Object(ARRAY(i1013)), i1014, i543, i567, matching1) → 2276_0_binarySearch_EQ(EOS(STATIC_2276), java.lang.Object(ARRAY(i1013)), i1014, i543, i567, 1) | =(matching1, 1)
2276_0_binarySearch_EQ(EOS(STATIC_2276), java.lang.Object(ARRAY(i1013)), i1014, i543, i567, matching1) → 2282_0_binarySearch_ConstantStackPush(EOS(STATIC_2282), java.lang.Object(ARRAY(i1013)), i1014, i543, i567) | &&(>(1, 0), =(matching1, 1))
2279_0_binarySearch_InvokeMethod(EOS(STATIC_2279), java.lang.Object(ARRAY(i1049)), i1050, i543, i567, java.lang.Object(ARRAY(i1049)), i1050, i1051, i1052, java.lang.Object(ARRAY(i1049)), i1050, i1052, i1048, java.lang.Object(ARRAY(i1049)), i1050, i1051, i785) → 2291_0_binarySearch_InvokeMethod(EOS(STATIC_2291), java.lang.Object(ARRAY(i1049)), i1050, i543, i567, java.lang.Object(ARRAY(i1049)), i1050, i1051, i1052)
2282_0_binarySearch_ConstantStackPush(EOS(STATIC_2282), java.lang.Object(ARRAY(i1013)), i1014, i543, i567) → 2294_0_binarySearch_Return(EOS(STATIC_2294), java.lang.Object(ARRAY(i1013)), i1014, i543, i567, 1)
2291_0_binarySearch_InvokeMethod(EOS(STATIC_2291), java.lang.Object(ARRAY(i1049)), i1050, i543, i567, java.lang.Object(ARRAY(i1049)), i1050, i1051, i1052) → 2465_0_binarySearch_InvokeMethod(EOS(STATIC_2465), java.lang.Object(ARRAY(i1049)), i1050, i543, i567, java.lang.Object(ARRAY(i1049)), i1050, i1051, i1052)
2327_0_binarySearch_InvokeMethod(EOS(STATIC_2327), java.lang.Object(ARRAY(i1086)), i1087, i543, i567, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1089, java.lang.Object(ARRAY(i1086)), i1087, i1089, i1085, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1052) → 2279_0_binarySearch_InvokeMethod(EOS(STATIC_2279), java.lang.Object(ARRAY(i1086)), i1087, i543, i567, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1089, java.lang.Object(ARRAY(i1086)), i1087, i1089, i1085, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1052)
2337_1_binarySearch_InvokeMethod(1880_0_binarySearch_Return(EOS(STATIC_1880), java.lang.Object(ARRAY(i1137)), i1138, i1139, i1140, matching1), java.lang.Object(ARRAY(i1137)), i1138, i1139, i1140) → 2368_0_binarySearch_Return(EOS(STATIC_2368), java.lang.Object(ARRAY(i1137)), i1138, i1139, i1140, java.lang.Object(ARRAY(i1137)), i1138, i1139, i1140, 0) | =(matching1, 0)
2337_1_binarySearch_InvokeMethod(1942_0_binarySearch_Return(EOS(STATIC_1942), java.lang.Object(ARRAY(i1144)), i1145, i1146, i1147, i567, matching1), java.lang.Object(ARRAY(i1144)), i1145, i1146, i1147) → 2369_0_binarySearch_Return(EOS(STATIC_2369), java.lang.Object(ARRAY(i1144)), i1145, i1146, i1147, java.lang.Object(ARRAY(i1144)), i1145, i1146, i1147, i567, 1) | =(matching1, 1)
2337_1_binarySearch_InvokeMethod(2084_0_binarySearch_ArrayAccess(EOS(STATIC_2084), java.lang.Object(ARRAY(i1151)), i1152, i1153, i1154, i566, java.lang.Object(ARRAY(i1151)), i566), java.lang.Object(ARRAY(i1151)), i1152, i1153, i1154) → 2371_0_binarySearch_ArrayAccess(EOS(STATIC_2371), java.lang.Object(ARRAY(i1151)), i1152, i1153, i1154, java.lang.Object(ARRAY(i1151)), i1152, i1153, i1154, i566, java.lang.Object(ARRAY(i1151)), i566)
2337_1_binarySearch_InvokeMethod(2118_0_binarySearch_ArrayAccess(EOS(STATIC_2118), java.lang.Object(ARRAY(i1158)), i1159, i1160, i1161, i567, java.lang.Object(ARRAY(i1158)), i567), java.lang.Object(ARRAY(i1158)), i1159, i1160, i1161) → 2377_0_binarySearch_ArrayAccess(EOS(STATIC_2377), java.lang.Object(ARRAY(i1158)), i1159, i1160, i1161, java.lang.Object(ARRAY(i1158)), i1159, i1160, i1161, i567, java.lang.Object(ARRAY(i1158)), i567)
2337_1_binarySearch_InvokeMethod(2216_0_binarySearch_InvokeMethod(EOS(STATIC_2216), java.lang.Object(ARRAY(i1166)), i1167, i1169, i567, java.lang.Object(ARRAY(i1166)), i1167, i1168, i785), java.lang.Object(ARRAY(i1166)), i1167, i1168, i1169) → 2379_0_binarySearch_InvokeMethod(EOS(STATIC_2379), java.lang.Object(ARRAY(i1166)), i1167, i1168, i1169, java.lang.Object(ARRAY(i1166)), i1167, i1169, i567, java.lang.Object(ARRAY(i1166)), i1167, i1168, i785)
2337_1_binarySearch_InvokeMethod(2291_0_binarySearch_InvokeMethod(EOS(STATIC_2291), java.lang.Object(ARRAY(i1173)), i1174, i1176, i567, java.lang.Object(ARRAY(i1173)), i1174, i1175, i1052), java.lang.Object(ARRAY(i1173)), i1174, i1175, i1176) → 2382_0_binarySearch_InvokeMethod(EOS(STATIC_2382), java.lang.Object(ARRAY(i1173)), i1174, i1175, i1176, java.lang.Object(ARRAY(i1173)), i1174, i1176, i567, java.lang.Object(ARRAY(i1173)), i1174, i1175, i1052)
2337_1_binarySearch_InvokeMethod(2294_0_binarySearch_Return(EOS(STATIC_2294), java.lang.Object(ARRAY(i1185)), i1186, i1188, i567, matching1), java.lang.Object(ARRAY(i1185)), i1186, i1187, i1188) → 2383_0_binarySearch_Return(EOS(STATIC_2383), java.lang.Object(ARRAY(i1185)), i1186, i1187, i1188, java.lang.Object(ARRAY(i1185)), i1186, i1188, i567, 1) | =(matching1, 1)
2337_1_binarySearch_InvokeMethod(2385_0_binarySearch_Return(EOS(STATIC_2385), matching1), java.lang.Object(ARRAY(i1301)), i1302, i1303, i1304) → 2441_0_binarySearch_Return(EOS(STATIC_2441), java.lang.Object(ARRAY(i1301)), i1302, i1303, i1304, 0) | =(matching1, 0)
2337_1_binarySearch_InvokeMethod(2394_0_binarySearch_InvokeMethod(EOS(STATIC_2394), java.lang.Object(ARRAY(i1319)), i1320, i1168, i1322), java.lang.Object(ARRAY(i1319)), i1320, i1321, i1322) → 2444_0_binarySearch_InvokeMethod(EOS(STATIC_2444), java.lang.Object(ARRAY(i1319)), i1320, i1321, i1322, java.lang.Object(ARRAY(i1319)), i1320, i1168, i1322)
2337_1_binarySearch_InvokeMethod(2397_0_binarySearch_Return(EOS(STATIC_2397), matching1), java.lang.Object(ARRAY(i1337)), i1338, i1339, i1340) → 2453_0_binarySearch_Return(EOS(STATIC_2453), java.lang.Object(ARRAY(i1337)), i1338, i1339, i1340, 1) | =(matching1, 1)
2337_1_binarySearch_InvokeMethod(2465_0_binarySearch_InvokeMethod(EOS(STATIC_2465), java.lang.Object(ARRAY(i1492)), i1493, i1495, i567, java.lang.Object(ARRAY(i1492)), i1493, i1494, i1315), java.lang.Object(ARRAY(i1492)), i1493, i1494, i1495) → 2529_0_binarySearch_InvokeMethod(EOS(STATIC_2529), java.lang.Object(ARRAY(i1492)), i1493, i1494, i1495, java.lang.Object(ARRAY(i1492)), i1493, i1495, i567, java.lang.Object(ARRAY(i1492)), i1493, i1494, i1315)
2337_1_binarySearch_InvokeMethod(2469_0_binarySearch_InvokeMethod(EOS(STATIC_2469), java.lang.Object(ARRAY(i1510)), i1511, i1321, i1513), java.lang.Object(ARRAY(i1510)), i1511, i1512, i1513) → 2539_0_binarySearch_InvokeMethod(EOS(STATIC_2539), java.lang.Object(ARRAY(i1510)), i1511, i1512, i1513, java.lang.Object(ARRAY(i1510)), i1511, i1321, i1513)
2337_1_binarySearch_InvokeMethod(2473_0_binarySearch_Return(EOS(STATIC_2473), i1372), java.lang.Object(ARRAY(i1529)), i1530, i1531, i1532) → 2545_0_binarySearch_Return(EOS(STATIC_2545), java.lang.Object(ARRAY(i1529)), i1530, i1531, i1532, i1372)
2368_0_binarySearch_Return(EOS(STATIC_2368), java.lang.Object(ARRAY(i1137)), i1138, i1139, i1140, java.lang.Object(ARRAY(i1137)), i1138, i1139, i1140, matching1) → 2385_0_binarySearch_Return(EOS(STATIC_2385), 0) | =(matching1, 0)
2369_0_binarySearch_Return(EOS(STATIC_2369), java.lang.Object(ARRAY(i1144)), i1145, i1146, i1147, java.lang.Object(ARRAY(i1144)), i1145, i1146, i1147, i567, matching1) → 2388_0_binarySearch_Return(EOS(STATIC_2388), 1) | =(matching1, 1)
2371_0_binarySearch_ArrayAccess(EOS(STATIC_2371), java.lang.Object(ARRAY(i1151)), i1152, i1153, i1154, java.lang.Object(ARRAY(i1151)), i1152, i1153, i1154, i566, java.lang.Object(ARRAY(i1151)), i566) → 2378_0_binarySearch_ArrayAccess(EOS(STATIC_2378), java.lang.Object(ARRAY(i1151)), i1152, i1153, i1154, java.lang.Object(ARRAY(i1151)), i1152, i1153, i1154, i566, java.lang.Object(ARRAY(i1151)), i566)
2377_0_binarySearch_ArrayAccess(EOS(STATIC_2377), java.lang.Object(ARRAY(i1158)), i1159, i1160, i1161, java.lang.Object(ARRAY(i1158)), i1159, i1160, i1161, i567, java.lang.Object(ARRAY(i1158)), i567) → 2378_0_binarySearch_ArrayAccess(EOS(STATIC_2378), java.lang.Object(ARRAY(i1158)), i1159, i1160, i1161, java.lang.Object(ARRAY(i1158)), i1159, i1160, i1161, i567, java.lang.Object(ARRAY(i1158)), i567)
2378_0_binarySearch_ArrayAccess(EOS(STATIC_2378), java.lang.Object(ARRAY(i1191)), i1192, i1196, i1193, java.lang.Object(ARRAY(i1191)), i1192, i1196, i1193, i1197, java.lang.Object(ARRAY(i1191)), i1197) → 2390_0_binarySearch_InvokeMethod(EOS(STATIC_2390), java.lang.Object(ARRAY(i1191)), i1192, i1196, i1193)
2379_0_binarySearch_InvokeMethod(EOS(STATIC_2379), java.lang.Object(ARRAY(i1166)), i1167, i1168, i1169, java.lang.Object(ARRAY(i1166)), i1167, i1169, i567, java.lang.Object(ARRAY(i1166)), i1167, i1168, i785) → 2394_0_binarySearch_InvokeMethod(EOS(STATIC_2394), java.lang.Object(ARRAY(i1166)), i1167, i1168, i1169)
2382_0_binarySearch_InvokeMethod(EOS(STATIC_2382), java.lang.Object(ARRAY(i1173)), i1174, i1175, i1176, java.lang.Object(ARRAY(i1173)), i1174, i1176, i567, java.lang.Object(ARRAY(i1173)), i1174, i1175, i1052) → 2379_0_binarySearch_InvokeMethod(EOS(STATIC_2379), java.lang.Object(ARRAY(i1173)), i1174, i1175, i1176, java.lang.Object(ARRAY(i1173)), i1174, i1176, i567, java.lang.Object(ARRAY(i1173)), i1174, i1175, i1052)
2383_0_binarySearch_Return(EOS(STATIC_2383), java.lang.Object(ARRAY(i1185)), i1186, i1187, i1188, java.lang.Object(ARRAY(i1185)), i1186, i1188, i567, matching1) → 2397_0_binarySearch_Return(EOS(STATIC_2397), 1) | =(matching1, 1)
2385_0_binarySearch_Return(EOS(STATIC_2385), matching1) → 2473_0_binarySearch_Return(EOS(STATIC_2473), 0) | =(matching1, 0)
2388_0_binarySearch_Return(EOS(STATIC_2388), matching1) → 2397_0_binarySearch_Return(EOS(STATIC_2397), 1) | =(matching1, 1)
2390_0_binarySearch_InvokeMethod(EOS(STATIC_2390), java.lang.Object(ARRAY(i1191)), i1192, i1196, i1193) → 2394_0_binarySearch_InvokeMethod(EOS(STATIC_2394), java.lang.Object(ARRAY(i1191)), i1192, i1196, i1193)
2394_0_binarySearch_InvokeMethod(EOS(STATIC_2394), java.lang.Object(ARRAY(i1166)), i1167, i1168, i1169) → 2469_0_binarySearch_InvokeMethod(EOS(STATIC_2469), java.lang.Object(ARRAY(i1166)), i1167, i1168, i1169)
2397_0_binarySearch_Return(EOS(STATIC_2397), matching1) → 2473_0_binarySearch_Return(EOS(STATIC_2473), 1) | =(matching1, 1)
2441_0_binarySearch_Return(EOS(STATIC_2441), java.lang.Object(ARRAY(i1301)), i1302, i1303, i1304, matching1) → 2454_0_binarySearch_Return(EOS(STATIC_2454), java.lang.Object(ARRAY(i1301)), i1302, i1303, i1304, 0) | =(matching1, 0)
2443_0_binarySearch_InvokeMethod(EOS(STATIC_2443), java.lang.Object(ARRAY(i1312)), i1313, i543, i567, java.lang.Object(ARRAY(i1312)), i1313, i1314, i1315, java.lang.Object(ARRAY(i1312)), i1313, i1168, i1315) → 2465_0_binarySearch_InvokeMethod(EOS(STATIC_2465), java.lang.Object(ARRAY(i1312)), i1313, i543, i567, java.lang.Object(ARRAY(i1312)), i1313, i1314, i1315)
2444_0_binarySearch_InvokeMethod(EOS(STATIC_2444), java.lang.Object(ARRAY(i1319)), i1320, i1321, i1322, java.lang.Object(ARRAY(i1319)), i1320, i1168, i1322) → 2469_0_binarySearch_InvokeMethod(EOS(STATIC_2469), java.lang.Object(ARRAY(i1319)), i1320, i1321, i1322)
2453_0_binarySearch_Return(EOS(STATIC_2453), java.lang.Object(ARRAY(i1337)), i1338, i1339, i1340, matching1) → 2454_0_binarySearch_Return(EOS(STATIC_2454), java.lang.Object(ARRAY(i1337)), i1338, i1339, i1340, 1) | =(matching1, 1)
2454_0_binarySearch_Return(EOS(STATIC_2454), java.lang.Object(ARRAY(i1367)), i1368, i1373, i1369, i1372) → 2473_0_binarySearch_Return(EOS(STATIC_2473), i1372)
2525_0_binarySearch_InvokeMethod(EOS(STATIC_2525), java.lang.Object(ARRAY(i1485)), i1486, i543, i567, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1488, java.lang.Object(ARRAY(i1485)), i1486, i1488, i1484, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1315) → 2279_0_binarySearch_InvokeMethod(EOS(STATIC_2279), java.lang.Object(ARRAY(i1485)), i1486, i543, i567, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1488, java.lang.Object(ARRAY(i1485)), i1486, i1488, i1484, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1315)
2529_0_binarySearch_InvokeMethod(EOS(STATIC_2529), java.lang.Object(ARRAY(i1492)), i1493, i1494, i1495, java.lang.Object(ARRAY(i1492)), i1493, i1495, i567, java.lang.Object(ARRAY(i1492)), i1493, i1494, i1315) → 2379_0_binarySearch_InvokeMethod(EOS(STATIC_2379), java.lang.Object(ARRAY(i1492)), i1493, i1494, i1495, java.lang.Object(ARRAY(i1492)), i1493, i1495, i567, java.lang.Object(ARRAY(i1492)), i1493, i1494, i1315)
2535_0_binarySearch_InvokeMethod(EOS(STATIC_2535), java.lang.Object(ARRAY(i1503)), i1504, i543, i567, java.lang.Object(ARRAY(i1503)), i1504, i1505, i1506, java.lang.Object(ARRAY(i1503)), i1504, i1321, i1506) → 2443_0_binarySearch_InvokeMethod(EOS(STATIC_2443), java.lang.Object(ARRAY(i1503)), i1504, i543, i567, java.lang.Object(ARRAY(i1503)), i1504, i1505, i1506, java.lang.Object(ARRAY(i1503)), i1504, i1321, i1506)
2539_0_binarySearch_InvokeMethod(EOS(STATIC_2539), java.lang.Object(ARRAY(i1510)), i1511, i1512, i1513, java.lang.Object(ARRAY(i1510)), i1511, i1321, i1513) → 2444_0_binarySearch_InvokeMethod(EOS(STATIC_2444), java.lang.Object(ARRAY(i1510)), i1511, i1512, i1513, java.lang.Object(ARRAY(i1510)), i1511, i1321, i1513)
2545_0_binarySearch_Return(EOS(STATIC_2545), java.lang.Object(ARRAY(i1529)), i1530, i1531, i1532, i1372) → 2454_0_binarySearch_Return(EOS(STATIC_2454), java.lang.Object(ARRAY(i1529)), i1530, i1531, i1532, i1372)
Combined rules. Obtained 7 conditional rules for P and 20 conditional rules for R.
P rules:
1869_0_binarySearch_Load(EOS(STATIC_1869), java.lang.Object(ARRAY(x0)), x1, x2, x3, x2) → 1975_1_binarySearch_InvokeMethod(1869_0_binarySearch_Load(EOS(STATIC_1869), java.lang.Object(ARRAY(x0)), x1, x2, -(+(x2, /(-(x3, x2), 2)), 1), x2), java.lang.Object(ARRAY(x0)), x1, x3, +(x2, /(-(x3, x2), 2)), java.lang.Object(ARRAY(x0)), x1, x2, -(+(x2, /(-(x3, x2), 2)), 1)) | &&(&&(>=(x3, x2), >(x0, +(x2, /(-(x3, x2), 2)))), <=(0, +(x2, /(-(x3, x2), 2))))
1975_1_binarySearch_InvokeMethod(1880_0_binarySearch_Return(EOS(STATIC_1880), java.lang.Object(ARRAY(x0)), x1, x2, x3, 0), java.lang.Object(ARRAY(x0)), x1, x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2337_1_binarySearch_InvokeMethod(1869_0_binarySearch_Load(EOS(STATIC_1869), java.lang.Object(ARRAY(x0)), x1, +(x6, 1), x5, +(x6, 1)), java.lang.Object(ARRAY(x0)), x1, +(x6, 1), x5) | >(+(x6, 1), 0)
1975_1_binarySearch_InvokeMethod(1942_0_binarySearch_Return(EOS(STATIC_1942), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5), java.lang.Object(ARRAY(x0)), x1, x6, x7, java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2337_1_binarySearch_InvokeMethod(1869_0_binarySearch_Load(EOS(STATIC_1869), java.lang.Object(ARRAY(x0)), x1, arith[3], x6, arith[3]), java.lang.Object(ARRAY(x0)), x1, arith[3], x6) | FALSE
1975_1_binarySearch_InvokeMethod(2294_0_binarySearch_Return(EOS(STATIC_2294), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4), java.lang.Object(ARRAY(x0)), x1, x5, x6, java.lang.Object(ARRAY(x0)), x1, x7, x2) → 2337_1_binarySearch_InvokeMethod(1869_0_binarySearch_Load(EOS(STATIC_1869), java.lang.Object(ARRAY(x0)), x1, arith[3], x5, arith[3]), java.lang.Object(ARRAY(x0)), x1, arith[3], x5) | FALSE
1975_1_binarySearch_InvokeMethod(2385_0_binarySearch_Return(EOS(STATIC_2385), 0), java.lang.Object(ARRAY(x1)), x2, x3, x4, java.lang.Object(ARRAY(x1)), x2, x5, x6) → 2337_1_binarySearch_InvokeMethod(1869_0_binarySearch_Load(EOS(STATIC_1869), java.lang.Object(ARRAY(x1)), x2, +(x4, 1), x3, +(x4, 1)), java.lang.Object(ARRAY(x1)), x2, +(x4, 1), x3) | >(+(x4, 1), 0)
1975_1_binarySearch_InvokeMethod(2397_0_binarySearch_Return(EOS(STATIC_2397), x0), java.lang.Object(ARRAY(x1)), x2, x3, x4, java.lang.Object(ARRAY(x1)), x2, x5, x6) → 2337_1_binarySearch_InvokeMethod(1869_0_binarySearch_Load(EOS(STATIC_1869), java.lang.Object(ARRAY(x1)), x2, arith[3], x3, arith[3]), java.lang.Object(ARRAY(x1)), x2, arith[3], x3) | FALSE
1975_1_binarySearch_InvokeMethod(2473_0_binarySearch_Return(EOS(STATIC_2473), 0), java.lang.Object(ARRAY(x1)), x2, x3, x4, java.lang.Object(ARRAY(x1)), x2, x5, x6) → 2337_1_binarySearch_InvokeMethod(1869_0_binarySearch_Load(EOS(STATIC_1869), java.lang.Object(ARRAY(x1)), x2, +(x4, 1), x3, +(x4, 1)), java.lang.Object(ARRAY(x1)), x2, +(x4, 1), x3) | >(+(x4, 1), 0)
R rules:
1975_1_binarySearch_InvokeMethod(2394_0_binarySearch_InvokeMethod(EOS(STATIC_2394), java.lang.Object(ARRAY(x0)), x1, x2, x3), java.lang.Object(ARRAY(x0)), x1, x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3) → 2465_0_binarySearch_InvokeMethod(EOS(STATIC_2465), java.lang.Object(ARRAY(x0)), x1, x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3)
1975_1_binarySearch_InvokeMethod(2469_0_binarySearch_InvokeMethod(EOS(STATIC_2469), java.lang.Object(ARRAY(x0)), x1, x2, x3), java.lang.Object(ARRAY(x0)), x1, x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3) → 2465_0_binarySearch_InvokeMethod(EOS(STATIC_2465), java.lang.Object(ARRAY(x0)), x1, x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3)
1975_1_binarySearch_InvokeMethod(2216_0_binarySearch_InvokeMethod(EOS(STATIC_2216), java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), java.lang.Object(ARRAY(x0)), x1, x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2) → 2465_0_binarySearch_InvokeMethod(EOS(STATIC_2465), java.lang.Object(ARRAY(x0)), x1, x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
1975_1_binarySearch_InvokeMethod(2291_0_binarySearch_InvokeMethod(EOS(STATIC_2291), java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), java.lang.Object(ARRAY(x0)), x1, x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2) → 2465_0_binarySearch_InvokeMethod(EOS(STATIC_2465), java.lang.Object(ARRAY(x0)), x1, x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
1975_1_binarySearch_InvokeMethod(2465_0_binarySearch_InvokeMethod(EOS(STATIC_2465), java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), java.lang.Object(ARRAY(x0)), x1, x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2) → 2465_0_binarySearch_InvokeMethod(EOS(STATIC_2465), java.lang.Object(ARRAY(x0)), x1, x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
1975_1_binarySearch_InvokeMethod(2084_0_binarySearch_ArrayAccess(EOS(STATIC_2084), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, java.lang.Object(ARRAY(x0)), x4), java.lang.Object(ARRAY(x0)), x1, x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2465_0_binarySearch_InvokeMethod(EOS(STATIC_2465), java.lang.Object(ARRAY(x0)), x1, x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3)
1975_1_binarySearch_InvokeMethod(2118_0_binarySearch_ArrayAccess(EOS(STATIC_2118), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, java.lang.Object(ARRAY(x0)), x4), java.lang.Object(ARRAY(x0)), x1, x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2465_0_binarySearch_InvokeMethod(EOS(STATIC_2465), java.lang.Object(ARRAY(x0)), x1, x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3)
2337_1_binarySearch_InvokeMethod(2394_0_binarySearch_InvokeMethod(EOS(STATIC_2394), java.lang.Object(ARRAY(x0)), x1, x2, x3), java.lang.Object(ARRAY(x0)), x1, x4, x3) → 2469_0_binarySearch_InvokeMethod(EOS(STATIC_2469), java.lang.Object(ARRAY(x0)), x1, x4, x3)
2337_1_binarySearch_InvokeMethod(2469_0_binarySearch_InvokeMethod(EOS(STATIC_2469), java.lang.Object(ARRAY(x0)), x1, x2, x3), java.lang.Object(ARRAY(x0)), x1, x4, x3) → 2469_0_binarySearch_InvokeMethod(EOS(STATIC_2469), java.lang.Object(ARRAY(x0)), x1, x4, x3)
2337_1_binarySearch_InvokeMethod(1880_0_binarySearch_Return(EOS(STATIC_1880), java.lang.Object(ARRAY(x0)), x1, x2, x3, 0), java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2473_0_binarySearch_Return(EOS(STATIC_2473), 0)
2337_1_binarySearch_InvokeMethod(2216_0_binarySearch_InvokeMethod(EOS(STATIC_2216), java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), java.lang.Object(ARRAY(x0)), x1, x4, x2) → 2469_0_binarySearch_InvokeMethod(EOS(STATIC_2469), java.lang.Object(ARRAY(x0)), x1, x4, x2)
2337_1_binarySearch_InvokeMethod(2291_0_binarySearch_InvokeMethod(EOS(STATIC_2291), java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), java.lang.Object(ARRAY(x0)), x1, x4, x2) → 2469_0_binarySearch_InvokeMethod(EOS(STATIC_2469), java.lang.Object(ARRAY(x0)), x1, x4, x2)
2337_1_binarySearch_InvokeMethod(2465_0_binarySearch_InvokeMethod(EOS(STATIC_2465), java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), java.lang.Object(ARRAY(x0)), x1, x4, x2) → 2469_0_binarySearch_InvokeMethod(EOS(STATIC_2469), java.lang.Object(ARRAY(x0)), x1, x4, x2)
2337_1_binarySearch_InvokeMethod(2084_0_binarySearch_ArrayAccess(EOS(STATIC_2084), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, java.lang.Object(ARRAY(x0)), x4), java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2469_0_binarySearch_InvokeMethod(EOS(STATIC_2469), java.lang.Object(ARRAY(x0)), x1, x2, x3)
2337_1_binarySearch_InvokeMethod(2118_0_binarySearch_ArrayAccess(EOS(STATIC_2118), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, java.lang.Object(ARRAY(x0)), x4), java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2469_0_binarySearch_InvokeMethod(EOS(STATIC_2469), java.lang.Object(ARRAY(x0)), x1, x2, x3)
2337_1_binarySearch_InvokeMethod(2294_0_binarySearch_Return(EOS(STATIC_2294), java.lang.Object(ARRAY(x0)), x1, x2, x3, 1), java.lang.Object(ARRAY(x0)), x1, x5, x2) → 2473_0_binarySearch_Return(EOS(STATIC_2473), 1)
2337_1_binarySearch_InvokeMethod(1942_0_binarySearch_Return(EOS(STATIC_1942), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, 1), java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2473_0_binarySearch_Return(EOS(STATIC_2473), 1)
2337_1_binarySearch_InvokeMethod(2385_0_binarySearch_Return(EOS(STATIC_2385), 0), java.lang.Object(ARRAY(x1)), x2, x3, x4) → 2473_0_binarySearch_Return(EOS(STATIC_2473), 0)
2337_1_binarySearch_InvokeMethod(2397_0_binarySearch_Return(EOS(STATIC_2397), 1), java.lang.Object(ARRAY(x1)), x2, x3, x4) → 2473_0_binarySearch_Return(EOS(STATIC_2473), 1)
2337_1_binarySearch_InvokeMethod(2473_0_binarySearch_Return(EOS(STATIC_2473), x0), java.lang.Object(ARRAY(x1)), x2, x3, x4) → 2473_0_binarySearch_Return(EOS(STATIC_2473), x0)
Filtered ground terms:
1869_0_binarySearch_Load(x1, x2, x3, x4, x5, x6) → 1869_0_binarySearch_Load(x2, x3, x4, x5, x6)
Cond_1975_1_binarySearch_InvokeMethod2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_1975_1_binarySearch_InvokeMethod2(x1, x3, x4, x5, x6, x7, x8, x9, x10)
2473_0_binarySearch_Return(x1, x2) → 2473_0_binarySearch_Return(x2)
Cond_1975_1_binarySearch_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_1975_1_binarySearch_InvokeMethod1(x1, x3, x4, x5, x6, x7, x8, x9, x10)
2385_0_binarySearch_Return(x1, x2) → 2385_0_binarySearch_Return
1880_0_binarySearch_Return(x1, x2, x3, x4, x5, x6) → 1880_0_binarySearch_Return(x2, x3, x4, x5)
Cond_1869_0_binarySearch_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_1869_0_binarySearch_Load(x1, x3, x4, x5, x6, x7)
2397_0_binarySearch_Return(x1, x2) → 2397_0_binarySearch_Return
1942_0_binarySearch_Return(x1, x2, x3, x4, x5, x6, x7) → 1942_0_binarySearch_Return(x2, x3, x4, x5, x6)
2294_0_binarySearch_Return(x1, x2, x3, x4, x5, x6) → 2294_0_binarySearch_Return(x2, x3, x4, x5)
2469_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5) → 2469_0_binarySearch_InvokeMethod(x2, x3, x4, x5)
2118_0_binarySearch_ArrayAccess(x1, x2, x3, x4, x5, x6, x7, x8) → 2118_0_binarySearch_ArrayAccess(x2, x3, x4, x5, x6, x7, x8)
2084_0_binarySearch_ArrayAccess(x1, x2, x3, x4, x5, x6, x7, x8) → 2084_0_binarySearch_ArrayAccess(x2, x3, x4, x5, x6, x7, x8)
2465_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9) → 2465_0_binarySearch_InvokeMethod(x2, x3, x4, x5, x6, x7, x8, x9)
2291_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9) → 2291_0_binarySearch_InvokeMethod(x2, x3, x4, x5, x6, x7, x8, x9)
2216_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9) → 2216_0_binarySearch_InvokeMethod(x2, x3, x4, x5, x6, x7, x8, x9)
2394_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5) → 2394_0_binarySearch_InvokeMethod(x2, x3, x4, x5)
Filtered duplicate args:
1869_0_binarySearch_Load(x1, x2, x3, x4, x5) → 1869_0_binarySearch_Load(x1, x2, x4, x5)
Cond_1869_0_binarySearch_Load(x1, x2, x3, x4, x5, x6) → Cond_1869_0_binarySearch_Load(x1, x2, x3, x5, x6)
1975_1_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9) → 1975_1_binarySearch_InvokeMethod(x1, x4, x5, x6, x7, x8, x9)
Cond_1975_1_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_1975_1_binarySearch_InvokeMethod(x1, x2, x5, x6)
Cond_1975_1_binarySearch_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_1975_1_binarySearch_InvokeMethod1(x1, x4, x5, x6, x7, x8, x9)
Cond_1975_1_binarySearch_InvokeMethod2(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_1975_1_binarySearch_InvokeMethod2(x1, x4, x5, x6, x7, x8, x9)
2465_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8) → 2465_0_binarySearch_InvokeMethod(x3, x4, x5, x6, x7, x8)
2216_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8) → 2216_0_binarySearch_InvokeMethod(x3, x4, x5, x6, x7, x8)
2291_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8) → 2291_0_binarySearch_InvokeMethod(x3, x4, x5, x6, x7, x8)
2084_0_binarySearch_ArrayAccess(x1, x2, x3, x4, x5, x6, x7) → 2084_0_binarySearch_ArrayAccess(x2, x3, x4, x6, x7)
2118_0_binarySearch_ArrayAccess(x1, x2, x3, x4, x5, x6, x7) → 2118_0_binarySearch_ArrayAccess(x2, x3, x4, x6, x7)
Filtered unneeded arguments:
Cond_1869_0_binarySearch_Load(x1, x2, x3, x4, x5) → Cond_1869_0_binarySearch_Load(x1, x2, x4, x5)
1975_1_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → 1975_1_binarySearch_InvokeMethod(x1, x2, x3, x4)
2337_1_binarySearch_InvokeMethod(x1, x2, x3, x4, x5) → 2337_1_binarySearch_InvokeMethod(x1)
Cond_1975_1_binarySearch_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7) → Cond_1975_1_binarySearch_InvokeMethod1(x1, x2, x3, x4)
Cond_1975_1_binarySearch_InvokeMethod2(x1, x2, x3, x4, x5, x6, x7) → Cond_1975_1_binarySearch_InvokeMethod2(x1, x2, x3, x4)
1869_0_binarySearch_Load(x1, x2, x3, x4) → 1869_0_binarySearch_Load(x1, x3, x4)
1880_0_binarySearch_Return(x1, x2, x3, x4) → 1880_0_binarySearch_Return(x1)
Combined rules. Obtained 4 conditional rules for P and 20 conditional rules for R.
P rules:
1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0)), x3, x2) → 1975_1_binarySearch_InvokeMethod(1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0)), -(+(x2, /(-(x3, x2), 2)), 1), x2), x3, +(x2, /(-(x3, x2), 2)), java.lang.Object(ARRAY(x0))) | &&(&&(>=(x3, x2), >(x0, +(x2, /(-(x3, x2), 2)))), <=(0, +(x2, /(-(x3, x2), 2))))
1975_1_binarySearch_InvokeMethod(1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0))), x5, x6, java.lang.Object(ARRAY(x0))) → 2337_1_binarySearch_InvokeMethod(1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0)), x5, +(x6, 1))) | >(x6, -1)
1975_1_binarySearch_InvokeMethod(2385_0_binarySearch_Return, x3, x4, java.lang.Object(ARRAY(x1))) → 2337_1_binarySearch_InvokeMethod(1869_0_binarySearch_Load(java.lang.Object(ARRAY(x1)), x3, +(x4, 1))) | >(x4, -1)
1975_1_binarySearch_InvokeMethod(2473_0_binarySearch_Return(0), x3, x4, java.lang.Object(ARRAY(x1))) → 2337_1_binarySearch_InvokeMethod(1869_0_binarySearch_Load(java.lang.Object(ARRAY(x1)), x3, +(x4, 1))) | >(x4, -1)
R rules:
1975_1_binarySearch_InvokeMethod(2394_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3), x4, x5, java.lang.Object(ARRAY(x0))) → 2465_0_binarySearch_InvokeMethod(x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3)
1975_1_binarySearch_InvokeMethod(2469_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3), x4, x5, java.lang.Object(ARRAY(x0))) → 2465_0_binarySearch_InvokeMethod(x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3)
1975_1_binarySearch_InvokeMethod(2216_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), x6, x7, java.lang.Object(ARRAY(x0))) → 2465_0_binarySearch_InvokeMethod(x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
1975_1_binarySearch_InvokeMethod(2291_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), x6, x7, java.lang.Object(ARRAY(x0))) → 2465_0_binarySearch_InvokeMethod(x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
1975_1_binarySearch_InvokeMethod(2465_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), x6, x7, java.lang.Object(ARRAY(x0))) → 2465_0_binarySearch_InvokeMethod(x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
1975_1_binarySearch_InvokeMethod(2084_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4), x5, x6, java.lang.Object(ARRAY(x0))) → 2465_0_binarySearch_InvokeMethod(x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3)
1975_1_binarySearch_InvokeMethod(2118_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4), x5, x6, java.lang.Object(ARRAY(x0))) → 2465_0_binarySearch_InvokeMethod(x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3)
2337_1_binarySearch_InvokeMethod(2394_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)) → 2469_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x3)
2337_1_binarySearch_InvokeMethod(2469_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)) → 2469_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x3)
2337_1_binarySearch_InvokeMethod(1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0)))) → 2473_0_binarySearch_Return(0)
2337_1_binarySearch_InvokeMethod(2216_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5)) → 2469_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x2)
2337_1_binarySearch_InvokeMethod(2291_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5)) → 2469_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x2)
2337_1_binarySearch_InvokeMethod(2465_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5)) → 2469_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x2)
2337_1_binarySearch_InvokeMethod(2084_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4)) → 2469_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)
2337_1_binarySearch_InvokeMethod(2118_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4)) → 2469_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)
2337_1_binarySearch_InvokeMethod(2294_0_binarySearch_Return(java.lang.Object(ARRAY(x0)), x1, x2, x3)) → 2473_0_binarySearch_Return(1)
2337_1_binarySearch_InvokeMethod(1942_0_binarySearch_Return(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4)) → 2473_0_binarySearch_Return(1)
2337_1_binarySearch_InvokeMethod(2385_0_binarySearch_Return) → 2473_0_binarySearch_Return(0)
2337_1_binarySearch_InvokeMethod(2397_0_binarySearch_Return) → 2473_0_binarySearch_Return(1)
2337_1_binarySearch_InvokeMethod(2473_0_binarySearch_Return(x0)) → 2473_0_binarySearch_Return(x0)
Performed bisimulation on rules. Used the following equivalence classes: {[2394_0_binarySearch_InvokeMethod_4, 2469_0_binarySearch_InvokeMethod_4, 2294_0_binarySearch_Return_4]=2394_0_binarySearch_InvokeMethod_4, [2465_0_binarySearch_InvokeMethod_6, 2216_0_binarySearch_InvokeMethod_6, 2291_0_binarySearch_InvokeMethod_6]=2465_0_binarySearch_InvokeMethod_6, [2084_0_binarySearch_ArrayAccess_5, 2118_0_binarySearch_ArrayAccess_5]=2084_0_binarySearch_ArrayAccess_5, [2385_0_binarySearch_Return, 2397_0_binarySearch_Return]=2385_0_binarySearch_Return}
Finished conversion. Obtained 9 rules for P and 12 rules for R. System has predefined symbols.
P rules:
1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0)), x3, x2) → COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3, x2), >(x0, +(x2, /(-(x3, x2), 2)))), <=(0, +(x2, /(-(x3, x2), 2)))), java.lang.Object(ARRAY(x0)), x3, x2)
COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x3, x2) → 1975_1_BINARYSEARCH_INVOKEMETHOD(1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0)), -(+(x2, /(-(x3, x2), 2)), 1), x2), x3, +(x2, /(-(x3, x2), 2)), java.lang.Object(ARRAY(x0)))
COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x3, x2) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0)), -(+(x2, /(-(x3, x2), 2)), 1), x2)
1975_1_BINARYSEARCH_INVOKEMETHOD(1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0))), x5, x6, java.lang.Object(ARRAY(x0))) → COND_1975_1_BINARYSEARCH_INVOKEMETHOD(>(x6, -1), 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0))), x5, x6, java.lang.Object(ARRAY(x0)))
COND_1975_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0))), x5, x6, java.lang.Object(ARRAY(x0))) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0)), x5, +(x6, 1))
1975_1_BINARYSEARCH_INVOKEMETHOD(2385_0_binarySearch_Return, x3, x4, java.lang.Object(ARRAY(x1))) → COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(>(x4, -1), 2385_0_binarySearch_Return, x3, x4, java.lang.Object(ARRAY(x1)))
COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2385_0_binarySearch_Return, x3, x4, java.lang.Object(ARRAY(x1))) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1)), x3, +(x4, 1))
1975_1_BINARYSEARCH_INVOKEMETHOD(2473_0_binarySearch_Return(0), x3, x4, java.lang.Object(ARRAY(x1))) → COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(>(x4, -1), 2473_0_binarySearch_Return(0), x3, x4, java.lang.Object(ARRAY(x1)))
COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2473_0_binarySearch_Return(0), x3, x4, java.lang.Object(ARRAY(x1))) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1)), x3, +(x4, 1))
R rules:
1975_1_binarySearch_InvokeMethod(2394_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3), x4, x5, java.lang.Object(ARRAY(x0))) → 2465_0_binarySearch_InvokeMethod(x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3)
1975_1_binarySearch_InvokeMethod(2465_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), x6, x7, java.lang.Object(ARRAY(x0))) → 2465_0_binarySearch_InvokeMethod(x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
1975_1_binarySearch_InvokeMethod(2084_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4), x5, x6, java.lang.Object(ARRAY(x0))) → 2465_0_binarySearch_InvokeMethod(x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3)
2337_1_binarySearch_InvokeMethod(2394_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)) → 2394_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x3)
2337_1_binarySearch_InvokeMethod(1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0)))) → 2473_0_binarySearch_Return(0)
2337_1_binarySearch_InvokeMethod(2465_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5)) → 2394_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x2)
2337_1_binarySearch_InvokeMethod(2084_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4)) → 2394_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)
2337_1_binarySearch_InvokeMethod(2394_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)) → 2473_0_binarySearch_Return(1)
2337_1_binarySearch_InvokeMethod(1942_0_binarySearch_Return(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4)) → 2473_0_binarySearch_Return(1)
2337_1_binarySearch_InvokeMethod(2385_0_binarySearch_Return) → 2473_0_binarySearch_Return(0)
2337_1_binarySearch_InvokeMethod(2385_0_binarySearch_Return) → 2473_0_binarySearch_Return(1)
2337_1_binarySearch_InvokeMethod(2473_0_binarySearch_Return(x0)) → 2473_0_binarySearch_Return(x0)
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Boolean, Integer
(0) -> (1), if (x3[0] >= x2[0] && x0[0] > x2[0] + x3[0] - x2[0] / 2 && 0 <= x2[0] + x3[0] - x2[0] / 2 ∧java.lang.Object(ARRAY(x0[0])) →* java.lang.Object(ARRAY(x0[1]))∧x3[0] →* x3[1]∧x2[0] →* x2[1])
(0) -> (2), if (x3[0] >= x2[0] && x0[0] > x2[0] + x3[0] - x2[0] / 2 && 0 <= x2[0] + x3[0] - x2[0] / 2 ∧java.lang.Object(ARRAY(x0[0])) →* java.lang.Object(ARRAY(x0[2]))∧x3[0] →* x3[2]∧x2[0] →* x2[2])
(1) -> (3), if (1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), x2[1] + x3[1] - x2[1] / 2 - 1, x2[1]) →* 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3])))∧x3[1] →* x5[3]∧x2[1] + x3[1] - x2[1] / 2 →* x6[3]∧java.lang.Object(ARRAY(x0[1])) →* java.lang.Object(ARRAY(x0[3])))
(1) -> (5), if (1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), x2[1] + x3[1] - x2[1] / 2 - 1, x2[1]) →* 2385_0_binarySearch_Return∧x3[1] →* x3[5]∧x2[1] + x3[1] - x2[1] / 2 →* x4[5]∧java.lang.Object(ARRAY(x0[1])) →* java.lang.Object(ARRAY(x1[5])))
(1) -> (7), if (1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), x2[1] + x3[1] - x2[1] / 2 - 1, x2[1]) →* 2473_0_binarySearch_Return(0)∧x3[1] →* x3[7]∧x2[1] + x3[1] - x2[1] / 2 →* x4[7]∧java.lang.Object(ARRAY(x0[1])) →* java.lang.Object(ARRAY(x1[7])))
(2) -> (0), if (java.lang.Object(ARRAY(x0[2])) →* java.lang.Object(ARRAY(x0[0]))∧x2[2] + x3[2] - x2[2] / 2 - 1 →* x3[0]∧x2[2] →* x2[0])
(3) -> (4), if (x6[3] > -1 ∧1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))) →* 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4])))∧x5[3] →* x5[4]∧x6[3] →* x6[4]∧java.lang.Object(ARRAY(x0[3])) →* java.lang.Object(ARRAY(x0[4])))
(4) -> (0), if (java.lang.Object(ARRAY(x0[4])) →* java.lang.Object(ARRAY(x0[0]))∧x5[4] →* x3[0]∧x6[4] + 1 →* x2[0])
(5) -> (6), if (x4[5] > -1 ∧x3[5] →* x3[6]∧x4[5] →* x4[6]∧java.lang.Object(ARRAY(x1[5])) →* java.lang.Object(ARRAY(x1[6])))
(6) -> (0), if (java.lang.Object(ARRAY(x1[6])) →* java.lang.Object(ARRAY(x0[0]))∧x3[6] →* x3[0]∧x4[6] + 1 →* x2[0])
(7) -> (8), if (x4[7] > -1 ∧x3[7] →* x3[8]∧x4[7] →* x4[8]∧java.lang.Object(ARRAY(x1[7])) →* java.lang.Object(ARRAY(x1[8])))
(8) -> (0), if (java.lang.Object(ARRAY(x1[8])) →* java.lang.Object(ARRAY(x0[0]))∧x3[8] →* x3[0]∧x4[8] + 1 →* x2[0])
(1) (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[1]))∧x3[0]=x3[1]∧x2[0]=x2[1] ⇒ 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))
(2) (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE ⇒ 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))
(3) (0 ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77 + (-1)Bound*bni_77] + [(-1)bni_77]x2[0] + [bni_77]x3[0] ≥ 0∧[(-1)bso_78] ≥ 0)
(4) (0 ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77 + (-1)Bound*bni_77] + [(-1)bni_77]x2[0] + [bni_77]x3[0] ≥ 0∧[(-1)bso_78] ≥ 0)
(5) (0 ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77 + (-1)Bound*bni_77] + [(-1)bni_77]x2[0] + [bni_77]x3[0] ≥ 0∧[(-1)bso_78] ≥ 0)
(6) (0 ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77] ≥ 0∧[bni_77] ≥ 0∧0 ≥ 0∧[(-1)bni_77 + (-1)Bound*bni_77] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_78] ≥ 0)
(7) (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[2]))∧x3[0]=x3[2]∧x2[0]=x2[2] ⇒ 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))
(8) (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE ⇒ 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))
(9) (0 ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77 + (-1)Bound*bni_77] + [(-1)bni_77]x2[0] + [bni_77]x3[0] ≥ 0∧[(-1)bso_78] ≥ 0)
(10) (0 ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77 + (-1)Bound*bni_77] + [(-1)bni_77]x2[0] + [bni_77]x3[0] ≥ 0∧[(-1)bso_78] ≥ 0)
(11) (0 ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77 + (-1)Bound*bni_77] + [(-1)bni_77]x2[0] + [bni_77]x3[0] ≥ 0∧[(-1)bso_78] ≥ 0)
(12) (0 ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77] ≥ 0∧[bni_77] ≥ 0∧0 ≥ 0∧[(-1)bni_77 + (-1)Bound*bni_77] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_78] ≥ 0)
(13) (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[1]))∧x3[0]=x3[1]∧x2[0]=x2[1] ⇒ COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x3[1], x2[1])≥NonInfC∧COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x3[1], x2[1])≥1975_1_BINARYSEARCH_INVOKEMETHOD(1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))∧(UIncreasing(1975_1_BINARYSEARCH_INVOKEMETHOD(1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))), ≥))
(14) (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE ⇒ COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥1975_1_BINARYSEARCH_INVOKEMETHOD(1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0[0])), -(+(x2[0], /(-(x3[0], x2[0]), 2)), 1), x2[0]), x3[0], +(x2[0], /(-(x3[0], x2[0]), 2)), java.lang.Object(ARRAY(x0[0])))∧(UIncreasing(1975_1_BINARYSEARCH_INVOKEMETHOD(1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))), ≥))
(15) (0 ≥ 0 ⇒ (UIncreasing(1975_1_BINARYSEARCH_INVOKEMETHOD(1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))), ≥)∧[(-1)bni_79 + (-1)Bound*bni_79] + [(-1)bni_79]x2[0] + [bni_79]x3[0] ≥ 0∧[2 + (-1)bso_80] + x2[0] ≥ 0)
(16) (0 ≥ 0 ⇒ (UIncreasing(1975_1_BINARYSEARCH_INVOKEMETHOD(1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))), ≥)∧[(-1)bni_79 + (-1)Bound*bni_79] + [(-1)bni_79]x2[0] + [bni_79]x3[0] ≥ 0∧[2 + (-1)bso_80] + x2[0] ≥ 0)
(17) (0 ≥ 0 ⇒ (UIncreasing(1975_1_BINARYSEARCH_INVOKEMETHOD(1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))), ≥)∧[(-1)bni_79 + (-1)Bound*bni_79] + [(-1)bni_79]x2[0] + [bni_79]x3[0] ≥ 0∧[2 + (-1)bso_80] + x2[0] ≥ 0)
(18) (0 ≥ 0 ⇒ (UIncreasing(1975_1_BINARYSEARCH_INVOKEMETHOD(1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))), ≥)∧[(-1)bni_79] ≥ 0∧[bni_79] ≥ 0∧0 ≥ 0∧[(-1)bni_79 + (-1)Bound*bni_79] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[2 + (-1)bso_80] ≥ 0)
(19) (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[2]))∧x3[0]=x3[2]∧x2[0]=x2[2] ⇒ COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2])≥NonInfC∧COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2])≥1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])∧(UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥))
(20) (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE ⇒ COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), -(+(x2[0], /(-(x3[0], x2[0]), 2)), 1), x2[0])∧(UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥))
(21) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_81 + (-1)Bound*bni_81] + [(-1)bni_81]x2[0] + [bni_81]x3[0] ≥ 0∧[(-1)bso_82] + x3[0] ≥ 0)
(22) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_81 + (-1)Bound*bni_81] + [(-1)bni_81]x2[0] + [bni_81]x3[0] ≥ 0∧[(-1)bso_82] + x3[0] ≥ 0)
(23) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_81 + (-1)Bound*bni_81] + [(-1)bni_81]x2[0] + [bni_81]x3[0] ≥ 0∧[(-1)bso_82] + x3[0] ≥ 0)
(24) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_81] ≥ 0∧[bni_81] ≥ 0∧0 ≥ 0∧[(-1)bni_81 + (-1)Bound*bni_81] ≥ 0∧0 ≥ 0∧[1] ≥ 0∧0 ≥ 0∧[(-1)bso_82] ≥ 0)
(25) (>(x6[3], -1)=TRUE∧1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3])))=1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4])))∧x5[3]=x5[4]∧x6[3]=x6[4]∧java.lang.Object(ARRAY(x0[3]))=java.lang.Object(ARRAY(x0[4])) ⇒ 1975_1_BINARYSEARCH_INVOKEMETHOD(1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))≥NonInfC∧1975_1_BINARYSEARCH_INVOKEMETHOD(1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))≥COND_1975_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))∧(UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))), ≥))
(26) (>(x6[3], -1)=TRUE ⇒ 1975_1_BINARYSEARCH_INVOKEMETHOD(1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))≥NonInfC∧1975_1_BINARYSEARCH_INVOKEMETHOD(1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))≥COND_1975_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))∧(UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))), ≥))
(27) (0 ≥ 0 ⇒ (UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))), ≥)∧[(-1)bni_83 + (-1)Bound*bni_83] + [(2)bni_83]x6[3] + [bni_83]x5[3] ≥ 0∧[(-1)bso_84] ≥ 0)
(28) (0 ≥ 0 ⇒ (UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))), ≥)∧[(-1)bni_83 + (-1)Bound*bni_83] + [(2)bni_83]x6[3] + [bni_83]x5[3] ≥ 0∧[(-1)bso_84] ≥ 0)
(29) (0 ≥ 0 ⇒ (UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))), ≥)∧[(-1)bni_83 + (-1)Bound*bni_83] + [(2)bni_83]x6[3] + [bni_83]x5[3] ≥ 0∧[(-1)bso_84] ≥ 0)
(30) (0 ≥ 0 ⇒ (UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))), ≥)∧0 ≥ 0∧[(2)bni_83] ≥ 0∧[bni_83] ≥ 0∧[(-1)bni_83 + (-1)Bound*bni_83] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_84] ≥ 0)
(31) (>(x6[3], -1)=TRUE∧1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3])))=1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4])))∧x5[3]=x5[4]∧x6[3]=x6[4]∧java.lang.Object(ARRAY(x0[3]))=java.lang.Object(ARRAY(x0[4]))∧java.lang.Object(ARRAY(x0[4]))=java.lang.Object(ARRAY(x0[0]))∧x5[4]=x3[0]∧+(x6[4], 1)=x2[0] ⇒ COND_1975_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4]))), x5[4], x6[4], java.lang.Object(ARRAY(x0[4])))≥NonInfC∧COND_1975_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4]))), x5[4], x6[4], java.lang.Object(ARRAY(x0[4])))≥1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))∧(UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))), ≥))
(32) (>(x6[3], -1)=TRUE ⇒ COND_1975_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))≥NonInfC∧COND_1975_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))≥1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[3])), x5[3], +(x6[3], 1))∧(UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))), ≥))
(33) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))), ≥)∧[(-1)bni_85 + (-1)Bound*bni_85] + [(2)bni_85]x6[3] + [bni_85]x5[3] ≥ 0∧[(-1)bso_86] + [2]x6[3] ≥ 0)
(34) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))), ≥)∧[(-1)bni_85 + (-1)Bound*bni_85] + [(2)bni_85]x6[3] + [bni_85]x5[3] ≥ 0∧[(-1)bso_86] + [2]x6[3] ≥ 0)
(35) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))), ≥)∧[(-1)bni_85 + (-1)Bound*bni_85] + [(2)bni_85]x6[3] + [bni_85]x5[3] ≥ 0∧[(-1)bso_86] + [2]x6[3] ≥ 0)
(36) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))), ≥)∧0 ≥ 0∧[(2)bni_85] ≥ 0∧[bni_85] ≥ 0∧[(-1)bni_85 + (-1)Bound*bni_85] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_86] ≥ 0∧[1] ≥ 0)
(37) (>(x4[5], -1)=TRUE∧x3[5]=x3[6]∧x4[5]=x4[6]∧java.lang.Object(ARRAY(x1[5]))=java.lang.Object(ARRAY(x1[6])) ⇒ 1975_1_BINARYSEARCH_INVOKEMETHOD(2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))≥NonInfC∧1975_1_BINARYSEARCH_INVOKEMETHOD(2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))≥COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))∧(UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))), ≥))
(38) (>(x4[5], -1)=TRUE ⇒ 1975_1_BINARYSEARCH_INVOKEMETHOD(2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))≥NonInfC∧1975_1_BINARYSEARCH_INVOKEMETHOD(2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))≥COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))∧(UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))), ≥))
(39) (0 ≥ 0 ⇒ (UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))), ≥)∧[(-1)bni_87 + (-1)Bound*bni_87] + [(2)bni_87]x4[5] + [bni_87]x3[5] ≥ 0∧[(-1)bso_88] ≥ 0)
(40) (0 ≥ 0 ⇒ (UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))), ≥)∧[(-1)bni_87 + (-1)Bound*bni_87] + [(2)bni_87]x4[5] + [bni_87]x3[5] ≥ 0∧[(-1)bso_88] ≥ 0)
(41) (0 ≥ 0 ⇒ (UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))), ≥)∧[(-1)bni_87 + (-1)Bound*bni_87] + [(2)bni_87]x4[5] + [bni_87]x3[5] ≥ 0∧[(-1)bso_88] ≥ 0)
(42) (0 ≥ 0 ⇒ (UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))), ≥)∧0 ≥ 0∧[(2)bni_87] ≥ 0∧[bni_87] ≥ 0∧[(-1)bni_87 + (-1)Bound*bni_87] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_88] ≥ 0)
(43) (>(x4[5], -1)=TRUE∧x3[5]=x3[6]∧x4[5]=x4[6]∧java.lang.Object(ARRAY(x1[5]))=java.lang.Object(ARRAY(x1[6]))∧java.lang.Object(ARRAY(x1[6]))=java.lang.Object(ARRAY(x0[0]))∧x3[6]=x3[0]∧+(x4[6], 1)=x2[0] ⇒ COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2385_0_binarySearch_Return, x3[6], x4[6], java.lang.Object(ARRAY(x1[6])))≥NonInfC∧COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2385_0_binarySearch_Return, x3[6], x4[6], java.lang.Object(ARRAY(x1[6])))≥1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))∧(UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))), ≥))
(44) (>(x4[5], -1)=TRUE ⇒ COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))≥NonInfC∧COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))≥1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[5])), x3[5], +(x4[5], 1))∧(UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))), ≥))
(45) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))), ≥)∧[(-1)bni_89 + (-1)Bound*bni_89] + [(2)bni_89]x4[5] + [bni_89]x3[5] ≥ 0∧[(-1)bso_90] + [2]x4[5] ≥ 0)
(46) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))), ≥)∧[(-1)bni_89 + (-1)Bound*bni_89] + [(2)bni_89]x4[5] + [bni_89]x3[5] ≥ 0∧[(-1)bso_90] + [2]x4[5] ≥ 0)
(47) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))), ≥)∧[(-1)bni_89 + (-1)Bound*bni_89] + [(2)bni_89]x4[5] + [bni_89]x3[5] ≥ 0∧[(-1)bso_90] + [2]x4[5] ≥ 0)
(48) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))), ≥)∧0 ≥ 0∧[(2)bni_89] ≥ 0∧[bni_89] ≥ 0∧[(-1)bni_89 + (-1)Bound*bni_89] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_90] ≥ 0∧[1] ≥ 0)
(49) (>(x4[7], -1)=TRUE∧x3[7]=x3[8]∧x4[7]=x4[8]∧java.lang.Object(ARRAY(x1[7]))=java.lang.Object(ARRAY(x1[8])) ⇒ 1975_1_BINARYSEARCH_INVOKEMETHOD(2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))≥NonInfC∧1975_1_BINARYSEARCH_INVOKEMETHOD(2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))≥COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))∧(UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))), ≥))
(50) (>(x4[7], -1)=TRUE ⇒ 1975_1_BINARYSEARCH_INVOKEMETHOD(2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))≥NonInfC∧1975_1_BINARYSEARCH_INVOKEMETHOD(2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))≥COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))∧(UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))), ≥))
(51) (0 ≥ 0 ⇒ (UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))), ≥)∧[(-1)bni_91 + (-1)Bound*bni_91] + [(2)bni_91]x4[7] + [bni_91]x3[7] ≥ 0∧[(-1)bso_92] ≥ 0)
(52) (0 ≥ 0 ⇒ (UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))), ≥)∧[(-1)bni_91 + (-1)Bound*bni_91] + [(2)bni_91]x4[7] + [bni_91]x3[7] ≥ 0∧[(-1)bso_92] ≥ 0)
(53) (0 ≥ 0 ⇒ (UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))), ≥)∧[(-1)bni_91 + (-1)Bound*bni_91] + [(2)bni_91]x4[7] + [bni_91]x3[7] ≥ 0∧[(-1)bso_92] ≥ 0)
(54) (0 ≥ 0 ⇒ (UIncreasing(COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))), ≥)∧0 ≥ 0∧[(2)bni_91] ≥ 0∧[bni_91] ≥ 0∧[(-1)bni_91 + (-1)Bound*bni_91] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_92] ≥ 0)
(55) (>(x4[7], -1)=TRUE∧x3[7]=x3[8]∧x4[7]=x4[8]∧java.lang.Object(ARRAY(x1[7]))=java.lang.Object(ARRAY(x1[8]))∧java.lang.Object(ARRAY(x1[8]))=java.lang.Object(ARRAY(x0[0]))∧x3[8]=x3[0]∧+(x4[8], 1)=x2[0] ⇒ COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2473_0_binarySearch_Return(0), x3[8], x4[8], java.lang.Object(ARRAY(x1[8])))≥NonInfC∧COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2473_0_binarySearch_Return(0), x3[8], x4[8], java.lang.Object(ARRAY(x1[8])))≥1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))∧(UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))), ≥))
(56) (>(x4[7], -1)=TRUE ⇒ COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))≥NonInfC∧COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))≥1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[7])), x3[7], +(x4[7], 1))∧(UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))), ≥))
(57) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))), ≥)∧[(-1)bni_93 + (-1)Bound*bni_93] + [(2)bni_93]x4[7] + [bni_93]x3[7] ≥ 0∧[(-1)bso_94] + [2]x4[7] ≥ 0)
(58) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))), ≥)∧[(-1)bni_93 + (-1)Bound*bni_93] + [(2)bni_93]x4[7] + [bni_93]x3[7] ≥ 0∧[(-1)bso_94] + [2]x4[7] ≥ 0)
(59) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))), ≥)∧[(-1)bni_93 + (-1)Bound*bni_93] + [(2)bni_93]x4[7] + [bni_93]x3[7] ≥ 0∧[(-1)bso_94] + [2]x4[7] ≥ 0)
(60) (0 ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))), ≥)∧0 ≥ 0∧[(2)bni_93] ≥ 0∧[bni_93] ≥ 0∧[(-1)bni_93 + (-1)Bound*bni_93] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_94] ≥ 0∧[1] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(1975_1_binarySearch_InvokeMethod(x1, x2, x3, x4)) = 0
POL(2394_0_binarySearch_InvokeMethod(x1, x2, x3, x4)) = 0
POL(java.lang.Object(x1)) = 0
POL(ARRAY(x1)) = 0
POL(2465_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6)) = 0
POL(2084_0_binarySearch_ArrayAccess(x1, x2, x3, x4, x5)) = 0
POL(2337_1_binarySearch_InvokeMethod(x1)) = 0
POL(1880_0_binarySearch_Return(x1)) = 0
POL(2473_0_binarySearch_Return(x1)) = 0
POL(0) = 0
POL(1) = 0
POL(1942_0_binarySearch_Return(x1, x2, x3, x4, x5)) = 0
POL(2385_0_binarySearch_Return) = 0
POL(1869_0_BINARYSEARCH_LOAD(x1, x2, x3)) = [-1] + [-1]x3 + x2 + [-1]x1
POL(COND_1869_0_BINARYSEARCH_LOAD(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3 + [-1]x2 + [2]x1
POL(&&(x1, x2)) = 0
POL(>=(x1, x2)) = 0
POL(>(x1, x2)) = 0
POL(+(x1, x2)) = 0
POL(-(x1, x2)) = 0
POL(2) = 0
POL(<=(x1, x2)) = 0
POL(1975_1_BINARYSEARCH_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + [-1]x4 + [2]x3 + x2 + [-1]x1
POL(1869_0_binarySearch_Load(x1, x2, x3)) = [2] + [2]x3 + x2
POL(COND_1975_1_BINARYSEARCH_INVOKEMETHOD(x1, x2, x3, x4, x5)) = [-1] + [-1]x5 + [2]x4 + x3 + [-1]x2
POL(-1) = 0
POL(COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(x1, x2, x3, x4, x5)) = [-1] + [-1]x5 + [2]x4 + x3 + [-1]x2
POL(COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(x1, x2, x3, x4, x5)) = [-1] + [-1]x5 + [2]x4 + x3 + [-1]x2
COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x3[1], x2[1]) → 1975_1_BINARYSEARCH_INVOKEMETHOD(1869_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))
1975_1_BINARYSEARCH_INVOKEMETHOD(1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3]))) → COND_1975_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))
COND_1975_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4]))), x5[4], x6[4], java.lang.Object(ARRAY(x0[4]))) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))
1975_1_BINARYSEARCH_INVOKEMETHOD(2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5]))) → COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))
COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2385_0_binarySearch_Return, x3[6], x4[6], java.lang.Object(ARRAY(x1[6]))) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))
1975_1_BINARYSEARCH_INVOKEMETHOD(2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7]))) → COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))
COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2473_0_binarySearch_Return(0), x3[8], x4[8], java.lang.Object(ARRAY(x1[8]))) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))
1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])
COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])
1975_1_BINARYSEARCH_INVOKEMETHOD(1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3]))) → COND_1975_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))
COND_1975_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4]))), x5[4], x6[4], java.lang.Object(ARRAY(x0[4]))) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))
1975_1_BINARYSEARCH_INVOKEMETHOD(2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5]))) → COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2385_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))
COND_1975_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2385_0_binarySearch_Return, x3[6], x4[6], java.lang.Object(ARRAY(x1[6]))) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))
1975_1_BINARYSEARCH_INVOKEMETHOD(2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7]))) → COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2473_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))
COND_1975_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2473_0_binarySearch_Return(0), x3[8], x4[8], java.lang.Object(ARRAY(x1[8]))) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))
&&(TRUE, TRUE)1 → TRUE1
&&(TRUE, FALSE)1 → FALSE1
&&(FALSE, TRUE)1 → FALSE1
&&(FALSE, FALSE)1 → FALSE1
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Boolean, Integer
(2) -> (0), if (java.lang.Object(ARRAY(x0[2])) →* java.lang.Object(ARRAY(x0[0]))∧x2[2] + x3[2] - x2[2] / 2 - 1 →* x3[0]∧x2[2] →* x2[0])
(4) -> (0), if (java.lang.Object(ARRAY(x0[4])) →* java.lang.Object(ARRAY(x0[0]))∧x5[4] →* x3[0]∧x6[4] + 1 →* x2[0])
(6) -> (0), if (java.lang.Object(ARRAY(x1[6])) →* java.lang.Object(ARRAY(x0[0]))∧x3[6] →* x3[0]∧x4[6] + 1 →* x2[0])
(8) -> (0), if (java.lang.Object(ARRAY(x1[8])) →* java.lang.Object(ARRAY(x0[0]))∧x3[8] →* x3[0]∧x4[8] + 1 →* x2[0])
(0) -> (2), if (x3[0] >= x2[0] && x0[0] > x2[0] + x3[0] - x2[0] / 2 && 0 <= x2[0] + x3[0] - x2[0] / 2 ∧java.lang.Object(ARRAY(x0[0])) →* java.lang.Object(ARRAY(x0[2]))∧x3[0] →* x3[2]∧x2[0] →* x2[2])
(3) -> (4), if (x6[3] > -1 ∧1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))) →* 1880_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4])))∧x5[3] →* x5[4]∧x6[3] →* x6[4]∧java.lang.Object(ARRAY(x0[3])) →* java.lang.Object(ARRAY(x0[4])))
(5) -> (6), if (x4[5] > -1 ∧x3[5] →* x3[6]∧x4[5] →* x4[6]∧java.lang.Object(ARRAY(x1[5])) →* java.lang.Object(ARRAY(x1[6])))
(7) -> (8), if (x4[7] > -1 ∧x3[7] →* x3[8]∧x4[7] →* x4[8]∧java.lang.Object(ARRAY(x1[7])) →* java.lang.Object(ARRAY(x1[8])))
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(2) -> (0), if (java.lang.Object(ARRAY(x0[2])) →* java.lang.Object(ARRAY(x0[0]))∧x2[2] + x3[2] - x2[2] / 2 - 1 →* x3[0]∧x2[2] →* x2[0])
(0) -> (2), if (x3[0] >= x2[0] && x0[0] > x2[0] + x3[0] - x2[0] / 2 && 0 <= x2[0] + x3[0] - x2[0] / 2 ∧java.lang.Object(ARRAY(x0[0])) →* java.lang.Object(ARRAY(x0[2]))∧x3[0] →* x3[2]∧x2[0] →* x2[2])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(2) -> (0), if (java.lang.Object(ARRAY(x0[2])) →* java.lang.Object(ARRAY(x0[0]))∧x2[2] + x3[2] - x2[2] / 2 - 1 →* x3[0]∧x2[2] →* x2[0])
(0) -> (2), if (x3[0] >= x2[0] && x0[0] > x2[0] + x3[0] - x2[0] / 2 && 0 <= x2[0] + x3[0] - x2[0] / 2 ∧java.lang.Object(ARRAY(x0[0])) →* java.lang.Object(ARRAY(x0[2]))∧x3[0] →* x3[2]∧x2[0] →* x2[2])
(1) (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[2]))∧x3[0]=x3[2]∧x2[0]=x2[2] ⇒ COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2])≥NonInfC∧COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2])≥1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])∧(UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥))
(2) (<=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE∧>=(x3[0], x2[0])=TRUE∧>(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE ⇒ COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), -(+(x2[0], /(-(x3[0], x2[0]), 2)), 1), x2[0])∧(UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥))
(3) (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x2[0] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] + [-1]x2[0] + x3[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0)
(4) (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x2[0] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] + [-1]x2[0] + x3[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0)
(5) (x3[0] + [-1]x2[0] ≥ 0∧[2]x3[0] + [-2]x2[0] ≥ 0∧[-1] + x3[0] ≥ 0∧x0[0] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x2[0] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(6) (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x2[0] + [-1] + x3[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(7) (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(8) (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(9) (x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(10) (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[2]))∧x3[0]=x3[2]∧x2[0]=x2[2] ⇒ 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))
(11) (<=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE∧>=(x3[0], x2[0])=TRUE∧>(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE ⇒ 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))
(12) (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[0] + [bni_28]x3[0] ≥ 0∧[1 + (-1)bso_29] ≥ 0)
(13) (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[0] + [bni_28]x3[0] ≥ 0∧[1 + (-1)bso_29] ≥ 0)
(14) (x3[0] + [-1]x2[0] ≥ 0∧[2]x3[0] + [-2]x2[0] ≥ 0∧[-1] + x3[0] ≥ 0∧x0[0] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[0] + [bni_28]x3[0] ≥ 0∧[1 + (-1)bso_29] ≥ 0)
(15) (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x2[0] + [-1] + x3[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[1 + (-1)bso_29] ≥ 0)
(16) (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[1 + (-1)bso_29] ≥ 0)
(17) (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)Bound*bni_28 + bni_28] + [bni_28]x3[0] ≥ 0∧[1 + (-1)bso_29] ≥ 0)
(18) (x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)Bound*bni_28 + bni_28] + [bni_28]x3[0] ≥ 0∧[1 + (-1)bso_29] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = [3]
POL(COND_1869_0_BINARYSEARCH_LOAD(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3 + [2]x2 + [-1]x1
POL(java.lang.Object(x1)) = [-1] + [-1]x1
POL(ARRAY(x1)) = [-1]
POL(1869_0_BINARYSEARCH_LOAD(x1, x2, x3)) = [1] + [-1]x3 + x2 + [-1]x1
POL(-(x1, x2)) = x1 + [-1]x2
POL(+(x1, x2)) = x1 + x2
POL(2) = [2]
POL(1) = [1]
POL(&&(x1, x2)) = [-1]
POL(>=(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(0) = 0
Polynomial Interpretations with Context Sensitive Arithemetic Replacement
POL(TermCSAR-Mode @ Context)
POL(/(x1, 2)1 @ {+_2/1}) = max{x1, [-1]x1} + [-1]
POL(/(x1, 2)-1 @ {+_2/1}) = max{x1, [-1]x1} + [-1]
POL(/(x1, 2)1 @ {1869_0_BINARYSEARCH_LOAD_3/1, -_2/0, +_2/1}) = max{x1, [-1]x1} + [-1]
1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])
COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])
1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])
COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])
/1 →
TRUE1 → &&(TRUE, TRUE)1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Boolean, Integer
(2) -> (0), if (java.lang.Object(ARRAY(x0[2])) →* java.lang.Object(ARRAY(x0[0]))∧x2[2] + x3[2] - x2[2] / 2 - 1 →* x3[0]∧x2[2] →* x2[0])
(0) -> (1), if (x3[0] >= x2[0] && x0[0] > x2[0] + x3[0] - x2[0] / 2 && 0 <= x2[0] + x3[0] - x2[0] / 2 ∧java.lang.Object(ARRAY(x0[0])) →* java.lang.Object(ARRAY(x0[1]))∧x3[0] →* x3[1]∧x2[0] →* x2[1])
(0) -> (2), if (x3[0] >= x2[0] && x0[0] > x2[0] + x3[0] - x2[0] / 2 && 0 <= x2[0] + x3[0] - x2[0] / 2 ∧java.lang.Object(ARRAY(x0[0])) →* java.lang.Object(ARRAY(x0[2]))∧x3[0] →* x3[2]∧x2[0] →* x2[2])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(2) -> (0), if (java.lang.Object(ARRAY(x0[2])) →* java.lang.Object(ARRAY(x0[0]))∧x2[2] + x3[2] - x2[2] / 2 - 1 →* x3[0]∧x2[2] →* x2[0])
(0) -> (2), if (x3[0] >= x2[0] && x0[0] > x2[0] + x3[0] - x2[0] / 2 && 0 <= x2[0] + x3[0] - x2[0] / 2 ∧java.lang.Object(ARRAY(x0[0])) →* java.lang.Object(ARRAY(x0[2]))∧x3[0] →* x3[2]∧x2[0] →* x2[2])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(2) -> (0), if (java.lang.Object(ARRAY(x0[2])) →* java.lang.Object(ARRAY(x0[0]))∧x2[2] + x3[2] - x2[2] / 2 - 1 →* x3[0]∧x2[2] →* x2[0])
(0) -> (2), if (x3[0] >= x2[0] && x0[0] > x2[0] + x3[0] - x2[0] / 2 && 0 <= x2[0] + x3[0] - x2[0] / 2 ∧java.lang.Object(ARRAY(x0[0])) →* java.lang.Object(ARRAY(x0[2]))∧x3[0] →* x3[2]∧x2[0] →* x2[2])
(1) (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[2]))∧x3[0]=x3[2]∧x2[0]=x2[2] ⇒ COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2])≥NonInfC∧COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2])≥1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])∧(UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥))
(2) (<=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE∧>=(x3[0], x2[0])=TRUE∧>(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE ⇒ COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), -(+(x2[0], /(-(x3[0], x2[0]), 2)), 1), x2[0])∧(UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥))
(3) (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [(-1)bni_23]x2[0] + [bni_23]x3[0] ≥ 0∧[2 + (-1)bso_27] + [-1]x2[0] + x3[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0)
(4) (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [(-1)bni_23]x2[0] + [bni_23]x3[0] ≥ 0∧[2 + (-1)bso_27] + [-1]x2[0] + x3[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0)
(5) (x3[0] + [-1]x2[0] ≥ 0∧[2]x3[0] + [-2]x2[0] ≥ 0∧[-1] + x3[0] ≥ 0∧x0[0] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [(-1)bni_23]x2[0] + [bni_23]x3[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)
(6) (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x2[0] + [-1] + x3[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)
(7) (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)
(8) (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)
(9) (x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0 ⇒ (UIncreasing(1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)
(10) (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[2]))∧x3[0]=x3[2]∧x2[0]=x2[2] ⇒ 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))
(11) (<=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE∧>=(x3[0], x2[0])=TRUE∧>(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE ⇒ 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))
(12) (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)Bound*bni_28] + [(-1)bni_28]x2[0] + [bni_28]x3[0] ≥ 0∧[(-1)bso_29] ≥ 0)
(13) (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)Bound*bni_28] + [(-1)bni_28]x2[0] + [bni_28]x3[0] ≥ 0∧[(-1)bso_29] ≥ 0)
(14) (x3[0] + [-1]x2[0] ≥ 0∧[2]x3[0] + [-2]x2[0] ≥ 0∧[-1] + x3[0] ≥ 0∧x0[0] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)Bound*bni_28] + [(-1)bni_28]x2[0] + [bni_28]x3[0] ≥ 0∧[(-1)bso_29] ≥ 0)
(15) (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x2[0] + [-1] + x3[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[(-1)bso_29] ≥ 0)
(16) (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[(-1)bso_29] ≥ 0)
(17) (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[(-1)bso_29] ≥ 0)
(18) (x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0 ⇒ (UIncreasing(COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[(-1)bso_29] ≥ 0)
POL(TRUE) = [2]
POL(FALSE) = [3]
POL(COND_1869_0_BINARYSEARCH_LOAD(x1, x2, x3, x4)) = [2] + [-1]x4 + x3 + [-1]x2 + [-1]x1
POL(java.lang.Object(x1)) = [-1] + [-1]x1
POL(ARRAY(x1)) = [-1]
POL(1869_0_BINARYSEARCH_LOAD(x1, x2, x3)) = [-1]x3 + x2 + [-1]x1
POL(-(x1, x2)) = x1 + [-1]x2
POL(+(x1, x2)) = x1 + x2
POL(2) = [2]
POL(1) = [1]
POL(&&(x1, x2)) = [2]
POL(>=(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(0) = 0
Polynomial Interpretations with Context Sensitive Arithemetic Replacement
POL(TermCSAR-Mode @ Context)
POL(/(x1, 2)1 @ {+_2/1}) = max{x1, [-1]x1} + [-1]
POL(/(x1, 2)-1 @ {+_2/1}) = max{x1, [-1]x1} + [-1]
POL(/(x1, 2)1 @ {1869_0_BINARYSEARCH_LOAD_3/1, -_2/0, +_2/1}) = max{x1, [-1]x1} + [-1]
COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])
COND_1869_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])
1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])
1869_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1869_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])
/1 →
&&(TRUE, TRUE)1 ↔ TRUE1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Boolean, Integer
Generated 30 rules for P and 0 rules for R.
P rules:
1231_0_createArray_Load(EOS(STATIC_1231), java.lang.Object(ARRAY(i77)), i314, i314) → 1238_0_createArray_ArrayLength(EOS(STATIC_1238), java.lang.Object(ARRAY(i77)), i314, i314, java.lang.Object(ARRAY(i77)))
1238_0_createArray_ArrayLength(EOS(STATIC_1238), java.lang.Object(ARRAY(i77)), i314, i314, java.lang.Object(ARRAY(i77))) → 1243_0_createArray_GE(EOS(STATIC_1243), java.lang.Object(ARRAY(i77)), i314, i314, i77) | >=(i77, 0)
1243_0_createArray_GE(EOS(STATIC_1243), java.lang.Object(ARRAY(i77)), i314, i314, i77) → 1252_0_createArray_GE(EOS(STATIC_1252), java.lang.Object(ARRAY(i77)), i314, i314, i77)
1252_0_createArray_GE(EOS(STATIC_1252), java.lang.Object(ARRAY(i77)), i314, i314, i77) → 1264_0_createArray_Load(EOS(STATIC_1264), java.lang.Object(ARRAY(i77)), i314) | <(i314, i77)
1264_0_createArray_Load(EOS(STATIC_1264), java.lang.Object(ARRAY(i77)), i314) → 1272_0_createArray_Load(EOS(STATIC_1272), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)))
1272_0_createArray_Load(EOS(STATIC_1272), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77))) → 1280_0_createArray_InvokeMethod(EOS(STATIC_1280), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314)
1280_0_createArray_InvokeMethod(EOS(STATIC_1280), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314) → 1290_0_random_FieldAccess(EOS(STATIC_1290), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314)
1290_0_random_FieldAccess(EOS(STATIC_1290), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314) → 1307_0_random_FieldAccess(EOS(STATIC_1307), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i75)))
1307_0_random_FieldAccess(EOS(STATIC_1307), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i75))) → 1317_0_random_ArrayAccess(EOS(STATIC_1317), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i75)), i313)
1317_0_random_ArrayAccess(EOS(STATIC_1317), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i75)), i313) → 1325_0_random_ArrayAccess(EOS(STATIC_1325), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i75)), i313)
1325_0_random_ArrayAccess(EOS(STATIC_1325), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i75)), i313) → 1334_0_random_Store(EOS(STATIC_1334), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, o381) | <(i313, i75)
1334_0_random_Store(EOS(STATIC_1334), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, o381) → 1344_0_random_FieldAccess(EOS(STATIC_1344), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, o381)
1344_0_random_FieldAccess(EOS(STATIC_1344), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, o381) → 1351_0_random_ConstantStackPush(EOS(STATIC_1351), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, o381, i313)
1351_0_random_ConstantStackPush(EOS(STATIC_1351), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, o381, i313) → 1358_0_random_IntArithmetic(EOS(STATIC_1358), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, o381, i313, 1)
1358_0_random_IntArithmetic(EOS(STATIC_1358), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, o381, i313, matching1) → 1364_0_random_FieldAccess(EOS(STATIC_1364), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, o381, +(i313, 1)) | &&(>(i313, 0), =(matching1, 1))
1364_0_random_FieldAccess(EOS(STATIC_1364), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, o381, i329) → 1371_0_random_Load(EOS(STATIC_1371), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, o381)
1371_0_random_Load(EOS(STATIC_1371), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, o381) → 1381_0_random_InvokeMethod(EOS(STATIC_1381), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, o381)
1381_0_random_InvokeMethod(EOS(STATIC_1381), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(o411sub)) → 1387_0_random_InvokeMethod(EOS(STATIC_1387), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(o411sub))
1387_0_random_InvokeMethod(EOS(STATIC_1387), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(o411sub)) → 1391_0_length_Load(EOS(STATIC_1391), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(o411sub), java.lang.Object(o411sub))
1391_0_length_Load(EOS(STATIC_1391), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(o411sub), java.lang.Object(o411sub)) → 1404_0_length_FieldAccess(EOS(STATIC_1404), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(o411sub), java.lang.Object(o411sub))
1404_0_length_FieldAccess(EOS(STATIC_1404), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(java.lang.String(o420sub, i361)), java.lang.Object(java.lang.String(o420sub, i361))) → 1408_0_length_FieldAccess(EOS(STATIC_1408), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(java.lang.String(o420sub, i361)), java.lang.Object(java.lang.String(o420sub, i361))) | &&(>=(i361, 0), >=(i362, 0))
1408_0_length_FieldAccess(EOS(STATIC_1408), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(java.lang.String(o420sub, i361)), java.lang.Object(java.lang.String(o420sub, i361))) → 1418_0_length_Return(EOS(STATIC_1418), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(java.lang.String(o420sub, i361)))
1418_0_length_Return(EOS(STATIC_1418), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314, java.lang.Object(java.lang.String(o420sub, i361))) → 1426_0_random_Return(EOS(STATIC_1426), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314)
1426_0_random_Return(EOS(STATIC_1426), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314) → 1432_0_createArray_ArrayAccess(EOS(STATIC_1432), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314)
1432_0_createArray_ArrayAccess(EOS(STATIC_1432), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314) → 1442_0_createArray_ArrayAccess(EOS(STATIC_1442), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314)
1442_0_createArray_ArrayAccess(EOS(STATIC_1442), java.lang.Object(ARRAY(i77)), i314, java.lang.Object(ARRAY(i77)), i314) → 1455_0_createArray_Inc(EOS(STATIC_1455), java.lang.Object(ARRAY(i77)), i314) | <(i314, i77)
1455_0_createArray_Inc(EOS(STATIC_1455), java.lang.Object(ARRAY(i77)), i314) → 1467_0_createArray_JMP(EOS(STATIC_1467), java.lang.Object(ARRAY(i77)), +(i314, 1)) | >=(i314, 0)
1467_0_createArray_JMP(EOS(STATIC_1467), java.lang.Object(ARRAY(i77)), i376) → 1478_0_createArray_Load(EOS(STATIC_1478), java.lang.Object(ARRAY(i77)), i376)
1478_0_createArray_Load(EOS(STATIC_1478), java.lang.Object(ARRAY(i77)), i376) → 1221_0_createArray_Load(EOS(STATIC_1221), java.lang.Object(ARRAY(i77)), i376)
1221_0_createArray_Load(EOS(STATIC_1221), java.lang.Object(ARRAY(i77)), i314) → 1231_0_createArray_Load(EOS(STATIC_1231), java.lang.Object(ARRAY(i77)), i314, i314)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
1231_0_createArray_Load(EOS(STATIC_1231), java.lang.Object(ARRAY(x0)), x1, x1) → 1231_0_createArray_Load(EOS(STATIC_1231), java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | &&(&&(>(+(x1, 1), 0), <(x1, x0)), >(+(x0, 1), 0))
R rules:
Filtered ground terms:
1231_0_createArray_Load(x1, x2, x3, x4) → 1231_0_createArray_Load(x2, x3, x4)
EOS(x1) → EOS
Cond_1231_0_createArray_Load(x1, x2, x3, x4, x5) → Cond_1231_0_createArray_Load(x1, x3, x4, x5)
Filtered duplicate args:
1231_0_createArray_Load(x1, x2, x3) → 1231_0_createArray_Load(x1, x3)
Cond_1231_0_createArray_Load(x1, x2, x3, x4) → Cond_1231_0_createArray_Load(x1, x2, x4)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
1231_0_createArray_Load(java.lang.Object(ARRAY(x0)), x1) → 1231_0_createArray_Load(java.lang.Object(ARRAY(x0)), +(x1, 1)) | &&(&&(>(x1, -1), <(x1, x0)), >(x0, -1))
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0)), x1) → COND_1231_0_CREATEARRAY_LOAD(&&(&&(>(x1, -1), <(x1, x0)), >(x0, -1)), java.lang.Object(ARRAY(x0)), x1)
COND_1231_0_CREATEARRAY_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x1) → 1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0)), +(x1, 1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Boolean, Integer
(0) -> (1), if (x1[0] > -1 && x1[0] < x0[0] && x0[0] > -1 ∧java.lang.Object(ARRAY(x0[0])) →* java.lang.Object(ARRAY(x0[1]))∧x1[0] →* x1[1])
(1) -> (0), if (java.lang.Object(ARRAY(x0[1])) →* java.lang.Object(ARRAY(x0[0]))∧x1[1] + 1 →* x1[0])
(1) (&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[1]))∧x1[0]=x1[1] ⇒ 1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0])≥NonInfC∧1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0])≥COND_1231_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])∧(UIncreasing(COND_1231_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥))
(2) (>(x0[0], -1)=TRUE∧>(x1[0], -1)=TRUE∧<(x1[0], x0[0])=TRUE ⇒ 1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0])≥NonInfC∧1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0])≥COND_1231_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])∧(UIncreasing(COND_1231_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥))
(3) (x0[0] ≥ 0∧x1[0] ≥ 0∧x0[0] + [-1] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_1231_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [(-1)bni_10]x1[0] + [bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)
(4) (x0[0] ≥ 0∧x1[0] ≥ 0∧x0[0] + [-1] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_1231_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [(-1)bni_10]x1[0] + [bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)
(5) (x0[0] ≥ 0∧x1[0] ≥ 0∧x0[0] + [-1] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_1231_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [(-1)bni_10]x1[0] + [bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)
(6) ([1] + x1[0] + x0[0] ≥ 0∧x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (UIncreasing(COND_1231_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥)∧[(-1)Bound*bni_10] + [bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)
(7) (COND_1231_0_CREATEARRAY_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1])≥NonInfC∧COND_1231_0_CREATEARRAY_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1])≥1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))∧(UIncreasing(1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥))
(8) ((UIncreasing(1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)
(9) ((UIncreasing(1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)
(10) ((UIncreasing(1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)
(11) ((UIncreasing(1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥)∧[bni_12] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(1231_0_CREATEARRAY_LOAD(x1, x2)) = [-1] + [-1]x2 + x1
POL(java.lang.Object(x1)) = x1
POL(ARRAY(x1)) = x1
POL(COND_1231_0_CREATEARRAY_LOAD(x1, x2, x3)) = [-1] + [-1]x3 + x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(-1) = [-1]
POL(<(x1, x2)) = [-1]
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
COND_1231_0_CREATEARRAY_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1]) → 1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))
1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0]) → COND_1231_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])
1231_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0]) → COND_1231_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Boolean, Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer